Merge pull request #3573 from mtzguido/nits2

Some nits

.docker/nu_base.Dockerfile

@@ -69,6 +69,8 @@ RUN sudo apt-get install -y --no-install-recommends \
 # To run Vale
 # RUN sudo apt-get install -y dotnet-runtime-6.0 dotnet-sdk-6.0
 
+RUN opam install --confirm-level=unsafe-yes mtime && opam clean
+
 # everparse (hex for quackyducky)
 RUN opam install --confirm-level=unsafe-yes hex sexplib re sha && opam clean
 

src/tactics/FStarC.Tactics.Printing.fst

@@ -168,7 +168,7 @@ let ps_to_json (msg, ps) =
                  else []))
 
 let do_dump_proofstate ps msg =
-    if not (Options.silent ()) then
+    if not (Options.silent ()) || Options.interactive () then
         Options.with_saved_options (fun () ->
             Options.set_option "print_effect_args" (Options.Bool true);
             print_generic "proof-state" ps_to_string ps_to_json (msg, ps);

src/tactics/FStarC.Tactics.V1.Basic.fst

@@ -157,7 +157,7 @@ let tacprint2 (s:string) x y   = BU.print1 "TAC>> %s\n" (BU.format2 s x y)
 let tacprint3 (s:string) x y z = BU.print1 "TAC>> %s\n" (BU.format3 s x y z)
 
 let print (msg:string) : tac unit =
-    if not (Options.silent ()) then
+    if not (Options.silent ()) || Options.interactive () then
       tacprint msg;
     ret ()
 

src/tactics/FStarC.Tactics.V2.Basic.fst

@@ -131,7 +131,7 @@ let tacprint2 (s:string) x y   = BU.print1 "TAC>> %s\n" (BU.format2 s x y)
 let tacprint3 (s:string) x y z = BU.print1 "TAC>> %s\n" (BU.format3 s x y z)
 
 let print (msg:string) : tac unit =
-    if not (Options.silent ()) then
+    if not (Options.silent ()) || Options.interactive () then
       tacprint msg;
     return ()
 

tests/error-messages/AQualMismatch.fst.expected

@@ -12,5 +12,3 @@
 * Warning 240 at AQualMismatch.fst(6,0-6,12):
   - Missing definitions in module AQualMismatch: f
 
-Verified module: AQualMismatch
-All verification conditions discharged successfully

tests/error-messages/AQualMismatch.fst.json_expected

@@ -3,5 +3,3 @@
 >>]
 {"msg":["AQualMismatch.f\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":3,"col":4},"end_pos":{"line":3,"col":5}}},"number":240,"ctx":["While desugaring module AQualMismatch"]}
 {"msg":["Missing definitions in module AQualMismatch: f"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"AQualMismatch.fst","start_pos":{"line":6,"col":0},"end_pos":{"line":6,"col":12}}},"number":240,"ctx":[]}
-Verified module: AQualMismatch
-All verification conditions discharged successfully

tests/error-messages/AnotType.fst.expected

@@ -9,5 +9,3 @@
   - Expected expression of type Type0 got expression tb of type Type
 
 >>]
-Verified module: AnotType
-All verification conditions discharged successfully

tests/error-messages/AnotType.fst.json_expected

@@ -4,5 +4,3 @@
 >> Got issues: [
 {"msg":["Expected expression of type Type0\ngot expression tb\nof type Type"],"level":"Error","range":{"def":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}},"use":{"file_name":"AnotType.fst","start_pos":{"line":27,"col":14},"end_pos":{"line":27,"col":16}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`","While typechecking the top-level declaration `[@@expect_failure] let uu___0`"]}
 >>]
-Verified module: AnotType
-All verification conditions discharged successfully

tests/error-messages/ArgsAndQuals.fst.expected

@@ -12,5 +12,3 @@
 * Warning 240 at ArgsAndQuals.fst(25,0-25,29):
   - Missing definitions in module ArgsAndQuals: test1
 
-Verified module: ArgsAndQuals
-All verification conditions discharged successfully

tests/error-messages/ArgsAndQuals.fst.json_expected

@@ -3,5 +3,3 @@
 >>]
 {"msg":["ArgsAndQuals.test1\nis declared but no definition was found","Add an 'assume' if this is intentional"],"level":"Warning","range":{"def":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":23,"col":4},"end_pos":{"line":23,"col":9}}},"number":240,"ctx":["While desugaring module ArgsAndQuals"]}
 {"msg":["Missing definitions in module ArgsAndQuals: test1"],"level":"Warning","range":{"def":{"file_name":"dummy","start_pos":{"line":0,"col":0},"end_pos":{"line":0,"col":0}},"use":{"file_name":"ArgsAndQuals.fst","start_pos":{"line":25,"col":0},"end_pos":{"line":25,"col":29}}},"number":240,"ctx":[]}
-Verified module: ArgsAndQuals
-All verification conditions discharged successfully

tests/error-messages/ArrowRanges.fst.expected

@@ -18,5 +18,3 @@
   - See also ArrowRanges.fst(7,0-11,1)
 
 >>]
-Verified module: ArrowRanges
-All verification conditions discharged successfully

tests/error-messages/ArrowRanges.fst.json_expected

@@ -4,5 +4,3 @@
 >> Got issues: [
 {"msg":["Failed to prove that the type\n'ArrowRanges.ppof'\nsupports decidable equality because of this argument.","Add either the 'noeq' or 'unopteq' qualifier","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"ArrowRanges.fst","start_pos":{"line":7,"col":0},"end_pos":{"line":11,"col":1}},"use":{"file_name":"ArrowRanges.fst","start_pos":{"line":8,"col":10},"end_pos":{"line":8,"col":28}}},"number":19,"ctx":["While typechecking the top-level declaration `type ArrowRanges.ppof`","While typechecking the top-level declaration `[@@expect_failure] type ArrowRanges.ppof`"]}
 >>]
-Verified module: ArrowRanges
-All verification conditions discharged successfully

tests/error-messages/AssertNorm.fst.expected

@@ -6,5 +6,3 @@
   - See also AssertNorm.fst(7,14-7,30)
 
 >>]
-Verified module: AssertNorm
-All verification conditions discharged successfully

tests/error-messages/AssertNorm.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":14},"end_pos":{"line":7,"col":30}},"use":{"file_name":"AssertNorm.fst","start_pos":{"line":7,"col":2},"end_pos":{"line":7,"col":13}}},"number":19,"ctx":["While typechecking the top-level declaration `let f`","While typechecking the top-level declaration `[@@expect_failure] let f`"]}
 >>]
-Verified module: AssertNorm
-All verification conditions discharged successfully

tests/error-messages/Asserts.fst.expected

@@ -21,5 +21,3 @@
   - See also Asserts.fst(16,9-16,14)
 
 >>]
-Verified module: Asserts
-All verification conditions discharged successfully

tests/error-messages/Asserts.fst.json_expected

@@ -7,5 +7,3 @@
 >> Got issues: [
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Asserts.fst","start_pos":{"line":16,"col":9},"end_pos":{"line":16,"col":14}},"use":{"file_name":"Asserts.fst","start_pos":{"line":16,"col":2},"end_pos":{"line":16,"col":8}}},"number":19,"ctx":["While typechecking the top-level declaration `let test3`","While typechecking the top-level declaration `[@@expect_failure] let test3`"]}
 >>]
-Verified module: Asserts
-All verification conditions discharged successfully

tests/error-messages/BadEmptyRecord.fst.expected

@@ -3,5 +3,3 @@
   - Could not resolve the type for this record.
 
 >>]
-Verified module: BadEmptyRecord
-All verification conditions discharged successfully

tests/error-messages/BadEmptyRecord.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["Could not resolve the type for this record."],"level":"Error","range":{"def":{"file_name":"BadEmptyRecord.fst","start_pos":{"line":9,"col":6},"end_pos":{"line":9,"col":8}},"use":{"file_name":"BadEmptyRecord.fst","start_pos":{"line":9,"col":6},"end_pos":{"line":9,"col":8}}},"number":360,"ctx":["While typechecking the top-level declaration `let test`","While typechecking the top-level declaration `[@@expect_failure] let test`"]}
 >>]
-Verified module: BadEmptyRecord
-All verification conditions discharged successfully

tests/error-messages/Basic.fst.expected

@@ -91,5 +91,3 @@
   - See also Prims.fst(451,90-451,102)
 
 >>]
-Verified module: Basic
-All verification conditions discharged successfully

tests/error-messages/Basic.fst.json_expected

@@ -34,5 +34,3 @@
 >> Got issues: [
 {"msg":["Assertion failed","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":451,"col":90},"end_pos":{"line":451,"col":102}},"use":{"file_name":"Basic.fst","start_pos":{"line":23,"col":46},"end_pos":{"line":23,"col":48}}},"number":19,"ctx":["While typechecking the top-level declaration `let test6`","While typechecking the top-level declaration `[@@expect_failure] let test6`"]}
 >>]
-Verified module: Basic
-All verification conditions discharged successfully

tests/error-messages/Bug1918.fst.expected

@@ -4,5 +4,3 @@
   - See also FStar.Tactics.Typeclasses.fst(297,6-300,7)
 
 >>]
-Verified module: Bug1918
-All verification conditions discharged successfully

tests/error-messages/Bug1918.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["Could not solve typeclass constraint `Bug1918.mon`"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Typeclasses.fst","start_pos":{"line":297,"col":6},"end_pos":{"line":300,"col":7}},"use":{"file_name":"Bug1918.fst","start_pos":{"line":11,"col":13},"end_pos":{"line":11,"col":14}}},"number":228,"ctx":["While synthesizing term with a tactic","Running tactic for meta-arg","While typechecking the top-level declaration `let comp2`","While typechecking the top-level declaration `[@@expect_failure] let comp2`"]}
 >>]
-Verified module: Bug1918
-All verification conditions discharged successfully

tests/error-messages/Bug1988.fst.expected

@@ -15,5 +15,3 @@
   - Prims.string is not a subtype of the expected type _: (*?u21*) _ -> (*?u22*) _
 
 >>]
-Verified module: Bug1988
-All verification conditions discharged successfully

tests/error-messages/Bug1988.fst.json_expected

@@ -7,5 +7,3 @@
 >> Got issues: [
 {"msg":["Prims.string is not a subtype of the expected type _: (*?u21*) _ -> (*?u22*) _"],"level":"Error","range":{"def":{"file_name":"Bug1988.fst","start_pos":{"line":21,"col":32},"end_pos":{"line":21,"col":38}},"use":{"file_name":"Bug1988.fst","start_pos":{"line":21,"col":32},"end_pos":{"line":21,"col":38}}},"number":54,"ctx":["While solving deferred constraints","solve_non_tactic_deferred_constraints","While typechecking the top-level declaration `let f2`","While typechecking the top-level declaration `[@@expect_failure] let f2`"]}
 >>]
-Verified module: Bug1988
-All verification conditions discharged successfully

tests/error-messages/Bug1997.fst.expected

@@ -416,5 +416,3 @@ private
 let _ = FStar.Pervasives.assert_norm (Bug1997.n0 == Bug1997.n1)
 ]
 
-Verified module: Bug1997
-All verification conditions discharged successfully

tests/error-messages/Bug1997.fst.json_expected

@@ -291,5 +291,3 @@ private
 let _ = FStar.Pervasives.assert_norm (Bug1997.n0 == Bug1997.n1)
 ]
 
-Verified module: Bug1997
-All verification conditions discharged successfully

tests/error-messages/Bug2010.fst.expected

@@ -5,5 +5,3 @@
     introduced for user-provided implicit term at Bug2010.fst(6,66-6,67)
 
 >>]
-Verified module: Bug2010
-All verification conditions discharged successfully

tests/error-messages/Bug2010.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["Failed to resolve implicit argument ?14\nof type Prims.nat\nintroduced for user-provided implicit term at Bug2010.fst(6,66-6,67)"],"level":"Error","range":{"def":{"file_name":"Bug2010.fst","start_pos":{"line":6,"col":66},"end_pos":{"line":6,"col":67}},"use":{"file_name":"Bug2010.fst","start_pos":{"line":6,"col":66},"end_pos":{"line":6,"col":67}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let concat'`","While typechecking the top-level declaration `[@@expect_failure] let concat'`"]}
 >>]
-Verified module: Bug2010
-All verification conditions discharged successfully

tests/error-messages/Bug2021.fst.expected

@@ -43,5 +43,3 @@
   - See also Bug2021.fst(36,11-36,12)
 
 >>]
-Verified module: Bug2021
-All verification conditions discharged successfully

tests/error-messages/Bug2021.fst.json_expected

@@ -16,5 +16,3 @@
 >> Got issues: [
 {"msg":["Failed to resolve implicit argument ?13\nof type Prims.int\nintroduced for Instantiating implicit argument"],"level":"Error","range":{"def":{"file_name":"Bug2021.fst","start_pos":{"line":36,"col":11},"end_pos":{"line":36,"col":12}},"use":{"file_name":"Bug2021.fst","start_pos":{"line":37,"col":13},"end_pos":{"line":37,"col":17}}},"number":66,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let test5`","While typechecking the top-level declaration `[@@expect_failure] let test5`"]}
 >>]
-Verified module: Bug2021
-All verification conditions discharged successfully

tests/error-messages/Bug2245.fst.expected

@@ -5,5 +5,3 @@
     of type Prims.int & Prims.int & Prims.int
 
 >>]
-Verified module: Bug2245
-All verification conditions discharged successfully

tests/error-messages/Bug2245.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["Expected expression of type (Prims.int & Prims.int) & Prims.int\ngot expression a\nof type Prims.int & Prims.int & Prims.int"],"level":"Error","range":{"def":{"file_name":"Bug2245.fst","start_pos":{"line":6,"col":23},"end_pos":{"line":6,"col":24}},"use":{"file_name":"Bug2245.fst","start_pos":{"line":6,"col":23},"end_pos":{"line":6,"col":24}}},"number":189,"ctx":["While typechecking the top-level declaration `let b`","While typechecking the top-level declaration `[@@expect_failure] let b`"]}
 >>]
-Verified module: Bug2245
-All verification conditions discharged successfully

tests/error-messages/Bug2820.fst.expected

@@ -17,5 +17,3 @@ let basic _ =
   () <: FStar.Pervasives.Lemma (ensures forall (x: Prims.int{x + 1 == 1 + x}). Prims.l_True)
 ]
 
-Verified module: Bug2820
-All verification conditions discharged successfully

tests/error-messages/Bug2820.fst.json_expected

@@ -17,5 +17,3 @@ let basic _ =
   () <: FStar.Pervasives.Lemma (ensures forall (x: Prims.int{x + 1 == 1 + x}). Prims.l_True)
 ]
 
-Verified module: Bug2820
-All verification conditions discharged successfully

tests/error-messages/Bug2899.fst.expected

@@ -35,5 +35,3 @@
   - See also FStar.Tactics.Effect.fsti(212,48-212,58)
 
 >>]
-Verified module: Bug2899
-All verification conditions discharged successfully

tests/error-messages/Bug2899.fst.json_expected

@@ -10,5 +10,3 @@
 >> Got issues: [
 {"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":17,"col":50},"end_pos":{"line":17,"col":66}}},"number":170,"ctx":["While preprocessing VC with a tactic","While typechecking the top-level declaration `let eval_tactic`","While typechecking the top-level declaration `[@@expect_failure] let eval_tactic`"]}
 >>]
-Verified module: Bug2899
-All verification conditions discharged successfully

tests/error-messages/Bug2953.fst.expected

@@ -3,5 +3,3 @@
   - When clauses are not yet supported in --verify mode; they will be some day
 
 >>]
-Verified module: Bug2953
-All verification conditions discharged successfully

tests/error-messages/Bug2953.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["When clauses are not yet supported in --verify mode; they will be some day"],"level":"Error","range":{"def":{"file_name":"Bug2953.fst","start_pos":{"line":14,"col":21},"end_pos":{"line":14,"col":31}},"use":{"file_name":"Bug2953.fst","start_pos":{"line":14,"col":21},"end_pos":{"line":14,"col":31}}},"number":236,"ctx":["While typechecking the top-level declaration `let open_view`","While typechecking the top-level declaration `[@@expect_failure] let open_view`"]}
 >>]
-Verified module: Bug2953
-All verification conditions discharged successfully

tests/error-messages/Bug2980.fst.expected

@@ -5,5 +5,3 @@
     of type _: Prims.int -> Type0
 
 >>]
-Verified module: Bug2980
-All verification conditions discharged successfully

tests/error-messages/Bug2980.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["Expected expression of type Type0\ngot expression Bug2980.t\nof type _: Prims.int -> Type0"],"level":"Error","range":{"def":{"file_name":"Bug2980.fst","start_pos":{"line":5,"col":4},"end_pos":{"line":5,"col":5}},"use":{"file_name":"Bug2980.fst","start_pos":{"line":5,"col":4},"end_pos":{"line":5,"col":5}}},"number":189,"ctx":["While typechecking the top-level declaration `type Bug2980.t`","While typechecking the top-level declaration `[@@expect_failure] type Bug2980.t`"]}
 >>]
-Verified module: Bug2980
-All verification conditions discharged successfully

tests/error-messages/Bug2981.fst.expected

@@ -7,5 +7,3 @@
   - Add explicit let-bindings to avoid this
 
 >>]
-Verified module: Bug2981
-All verification conditions discharged successfully

tests/error-messages/Bug2981.fst.json_expected

@@ -1,5 +1,3 @@
 >> Got issues: [
 {"msg":["Bound variable\n'g'\nescapes because of impure applications in the type of\n'check'","Add explicit let-bindings to avoid this"],"level":"Error","range":{"def":{"file_name":"Bug2981.fst","start_pos":{"line":10,"col":10},"end_pos":{"line":10,"col":27}},"use":{"file_name":"Bug2981.fst","start_pos":{"line":10,"col":10},"end_pos":{"line":10,"col":27}}},"number":56,"ctx":["While checking for escaped variables","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]}
 >>]
-Verified module: Bug2981
-All verification conditions discharged successfully

tests/error-messages/Bug3099.fst.expected

@@ -1,7 +0,0 @@
-proof-state: State dump @ depth 0 (X):
-Location: Bug3099.fst(11,50-11,64)
-Goal 1/1:
-(_: Prims.unit), (return_val: Prims.eqtype), (_: return_val == Prims.int & (Prims.int & (Prims.int & Prims.int))), (any_result: Prims.bool), (_: true == any_result), (any_result'0: Prims.logical), (_: Prims.l_True == any_result'0) |- _ : Prims.squash ((1, (2, (3, 4))) = (1, (2, (3, 4))))
-
-Verified module: Bug3099
-All verification conditions discharged successfully

tests/error-messages/Bug3099.fst.json_expected

@@ -1,7 +0,0 @@
-proof-state: State dump @ depth 0 (X):
-Location: Bug3099.fst(11,50-11,64)
-Goal 1/1:
-(_: Prims.unit), (return_val: Prims.eqtype), (_: return_val == Prims.int & (Prims.int & (Prims.int & Prims.int))), (any_result: Prims.bool), (_: true == any_result), (any_result'0: Prims.logical), (_: Prims.l_True == any_result'0) |- _ : Prims.squash ((1, (2, (3, 4))) = (1, (2, (3, 4))))
-
-Verified module: Bug3099
-All verification conditions discharged successfully

tests/error-messages/Bug3102.fst.expected

@@ -32,5 +32,3 @@
   - Add a type annotation that does not mention it
 
 >>]
-Verified module: Bug3102
-All verification conditions discharged successfully

tests/error-messages/Bug3102.fst.json_expected

@@ -16,5 +16,3 @@
 >> Got issues: [
 {"msg":["Bound variable\n'z'\nwould escape in the type of this letbinding","Add a type annotation that does not mention it"],"level":"Error","range":{"def":{"file_name":"Bug3102.fst","start_pos":{"line":49,"col":16},"end_pos":{"line":51,"col":7}},"use":{"file_name":"Bug3102.fst","start_pos":{"line":49,"col":16},"end_pos":{"line":51,"col":7}}},"number":56,"ctx":["While checking for escaped variables","While typechecking the top-level declaration `let g`","While typechecking the top-level declaration `[@@expect_failure] let g`"]}
 >>]
-Verified module: Bug3102
-All verification conditions discharged successfully

tests/error-messages/Bug3145.fst.expected

@@ -25,5 +25,3 @@ let t3 = Prims.int & (Prims.int & Prims.int)
 let t4 = Prims.int & Prims.int & Prims.int
 ]
 
-Verified module: Bug3145
-All verification conditions discharged successfully

tests/error-messages/Bug3145.fst.json_expected

@@ -25,5 +25,3 @@ let t3 = Prims.int & (Prims.int & Prims.int)
 let t4 = Prims.int & Prims.int & Prims.int
 ]
 
-Verified module: Bug3145
-All verification conditions discharged successfully

tests/error-messages/Bug3227.fst.expected

@@ -72,5 +72,3 @@ let test3 r = r.ff
 let test4 r x = r.ff x <: a
 ]
 
-Verified module: Bug3227
-All verification conditions discharged successfully

tests/error-messages/Bug3227.fst.json_expected

@@ -72,5 +72,3 @@ let test3 r = r.ff
 let test4 r x = r.ff x <: a
 ]
 
-Verified module: Bug3227
-All verification conditions discharged successfully

tests/error-messages/Bug3232b.fst.expected

@@ -12,5 +12,3 @@
 * Warning 240 at Bug3232b.fst(8,0-8,12):
   - Missing definitions in module Bug3232b: f
 
-Verified module: Bug3232b
-All verification conditions discharged successfully