Diff failed for files /tests/tactics/_output/Postprocess.fst.output and /tests/tactics/Postprocess.fst.output.expected: --- _output/Postprocess.fst.output 2025-02-14 22:35:29.485672041 +0000 +++ Postprocess.fst.output.expected 2025-02-14 22:30:49.977550358 +0000 @@ -482,11 +482,11 @@ [@ ] visible let apply_feq_lem : ($f:(uu___:a@1:(Tm_unknown) -> Tot b@1:(Tm_unknown)) -> $g:(uu___:a@2:(Tm_unknown) -> Tot b@2:(Tm_unknown)) -> Lemma (unit)) = (fun $f $g -> (congruence_fun f@1:(Tm_unknown) g@0:(Tm_unknown) ())) [@ ] -visible let fext : (uu___:unit -> Tac (unit)) = (fun uu___ -> let uu___#1098 : unit = (apply_lemma `(apply_feq_lem)[]) +visible let fext : (uu___:unit -> Tac (unit)) = (fun uu___ -> let uu___#1096 : unit = (apply_lemma `(apply_feq_lem)[]) in -let uu___#1099 : unit = (dismiss ()) +let uu___#1097 : unit = (dismiss ()) in -let uu___#1100 : (list binding) = (forall_intros ()) +let uu___#1098 : (list binding) = (forall_intros ()) in (ignore uu___@0:(Tm_unknown))) [@ ]

Process completed with exit code 2.

Process completed with exit code 1.

(271) * Warning 271 at /__w/FStar/FStar/FStar/stage0/out/bin/../lib/fstar/ulib/FStar.UInt.fsti(435,8-435,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.AST.fst(772,8-772,22): - Global binding 'FStarC.Parser.AST.decl_to_string' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(733,8-733,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(754,4-754,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1093,4-1093,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1731,4-1731,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fst(38,4-38,11): - Values of type `ambient` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val ambient` declaration for this symbol in the interface

(318) * Warning 318 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fst(56,4-56,13): - Values of type `inversion` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val inversion` declaration for this symbol in the interface

(345) * Warning 345 at /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(642,66-642,67): - Inserted an unsafe type coercion in generated code from unit -> 'a -> 'a to unit -> 'a -> 'b. - This may be unsound in F#. - See also /__w/FStar/FStar/FStar/ulib/FStar.Pervasives.fsti(642,55-642,56)

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(137,4-137,10): - Parameter 0 of subset is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(144,4-144,9): - Parameter 0 of equal is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteSet.Base.fst(151,4-151,12): - Parameter 0 of disjoint is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(345) * Warning 345: - Inserted an unsafe type coercion in generated code from some_ref -> (obj, obj) mreference to some_ref -> (unit, unit) mreference. - This may be unsound in F#.

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(83,4-83,10): - Parameter 0 of values is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(90,4-90,9): - Parameter 0 of items is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

(344) * Warning 344 at /__w/FStar/FStar/FStar/ulib/FStar.FiniteMap.Base.fst(138,4-138,9): - Parameter 0 of equal is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [0; ...]]` to the interface signature. - This type definition is being dropped

The Ubuntu-20.04 brownout takes place from 2025-02-01. For more details, see https://github.com/actions/runner-images/issues/11101

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(38,4-38,11): - Values of type `ambient` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val ambient` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(56,4-56,13): - Values of type `inversion` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val inversion` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(38,4-38,11): - Values of type `ambient` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val ambient` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(56,4-56,13): - Values of type `inversion` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val inversion` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Set.fst(25,4-25,9): - Values of type `equal` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val equal` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8): - Values of type `hide` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val hide` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(31,4-31,9): - Values of type `equal` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val equal` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(56,4-56,12): - Values of type `contains` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val contains` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(62,4-62,18): - Values of type `addr_unused_in` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val addr_unused_in` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(66,4-66,13): - Values of type `unused_in` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val unused_in` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(38,4-38,11): - Values of type `ambient` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val ambient` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(56,4-56,13): - Values of type `inversion` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val inversion` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Set.fst(25,4-25,9): - Values of type `equal` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val equal` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8): - Values of type `hide` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val hide` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(38,4-38,11): - Values of type `ambient` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val ambient` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(56,4-56,13): - Values of type `inversion` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val inversion` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(31,4-31,9): - Values of type `equal` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val equal` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(56,4-56,12): - Values of type `contains` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val contains` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(62,4-62,18): - Values of type `addr_unused_in` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val addr_unused_in` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(66,4-66,13): - Values of type `unused_in` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val unused_in` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(38,4-38,11): - Values of type `ambient` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val ambient` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(56,4-56,13): - Values of type `inversion` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val inversion` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(38,4-38,11): - Values of type `ambient` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val ambient` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Pervasives.fst(56,4-56,13): - Values of type `inversion` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val inversion` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Set.fst(25,4-25,9): - Values of type `equal` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val equal` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Ghost.fst(24,4-24,8): - Values of type `hide` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val hide` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/experimental/FStar.Witnessed.Core.fst(7,4-7,13): - Values of type `witnessed` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val witnessed` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(31,4-31,9): - Values of type `equal` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val equal` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(56,4-56,12): - Values of type `contains` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val contains` declaration for this symbol in the interface

(318) * Warning 318 at /home/runner/work/FStar/FStar/fstar/ulib/FStar.Monotonic.Heap.fst(62,4-62,18): - Values of type `addr_unused_in` will be erased during extraction, but its interface hides this fact. - Add the `erasable` attribute to the `val addr_unused_in` declaration for this symbol in the interface

(272) * Warning 272 at Hello.fst(5,0-5,34): - Top-level let-bindings must be total; this term may have effects

(350) * Warning 350 at Part2.Free.fst(132,4-134,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Free.fst(133,4-134,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.FreeFunExt.fst(136,4-138,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.FreeFunExt.fst(137,4-138,12): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Par.fst(40,18-40,40): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Par.fst(48,18-48,40): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.Par.fst(105,4-106,17): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.ST.fst(26,2-28,10): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

(350) * Warning 350 at Part2.ST.fst(27,2-28,10): - The lightweight do notation [x <-- y; z] or [x ;; z] is deprecated, use let operators (i.e. [let* x = y in z] or [y ;* z], [*] being any sequence of operator characters) instead.

time = 0.13

time = 0.14

time = 0.16

time = 0.19

time = 0.28

time = 0.46