From c3c92dd9107d0021686f11be8a5e1087f1eee9a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 15 Sep 2024 09:54:41 -0700 Subject: [PATCH 1/4] Respect case in module name checking, improve errors We do make an exception for Prims (in prims.fst), for the time being. Fixes #3474 --- src/fstar/FStar.Universal.fst | 11 ++++++++++- src/parser/FStar.Parser.Dep.fst | 10 ++++++---- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/src/fstar/FStar.Universal.fst b/src/fstar/FStar.Universal.fst index 6b305ae3ce5..f5b0c521e0c 100644 --- a/src/fstar/FStar.Universal.fst +++ b/src/fstar/FStar.Universal.fst @@ -103,8 +103,17 @@ let parse (env:uenv) (pre_fn: option string) (fn:string) with_dsenv_of_env env (FStar.ToSyntax.Interleave.initialize_interface lid1 decls1) in with_dsenv_of_env env (FStar.ToSyntax.Interleave.interleave_module ast true) + + | Parser.AST.Interface (lid1, _, _), Parser.AST.Module (lid2, _) -> + (* Names do not match *) + Errors.raise_error lid1 + Errors.Fatal_PreModuleMismatch + "Module name in implementation does not match that of interface." + | _ -> - Errors.raise_error0 Errors.Fatal_PreModuleMismatch "mismatch between pre-module and module" + Errors.raise_error0 + Errors.Fatal_PreModuleMismatch + "Module name in implementation does not match that of interface." in with_dsenv_of_env env (Desugar.ast_modul_to_modul ast) diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index 602cc7c56b1..d3afd007f91 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/src/parser/FStar.Parser.Dep.fst @@ -514,12 +514,14 @@ let namespace_of_lid l = String.concat "_" (List.map string_of_id (ns_of_lid l)) let check_module_declaration_against_filename (lid: lident) (filename: string): unit = - let k' = lowercase_join_longident lid true in - if String.lowercase (must (check_and_strip_suffix (basename filename))) <> k' then + let k' = string_of_lid lid true in + if must (check_and_strip_suffix (basename filename)) <> k' + && (not (basename filename = "prims.fst")) (* Exception for module Prims = prims.fst until we switch *) + then log_issue lid Errors.Error_ModuleFileNameMismatch [ Errors.Msg.text (Util.format2 "The module declaration \"module %s\" \ - found in file %s does not match its filename. Dependencies will be \ - incorrect and the module will not be verified." (string_of_lid lid true) filename) + found in file %s does not match its filename." (string_of_lid lid true) filename); + Errors.Msg.text "Dependencies will be incorrect and the module will not be verified."; ] exception Exit From 8e0a21d125187f2480365ad59d107aea49ffa0f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 15 Sep 2024 10:25:32 -0700 Subject: [PATCH 2/4] all: rename files to match modules --- examples/dm4free/{delimcc.fst => DelimCC.fst} | 0 examples/metatheory/{indind.fst => IndInd.fst} | 2 +- ...st => PropImpredicativeAndNonStrictlyPositiveInductives.fst} | 0 examples/rel/{label.fst => Label.fst} | 0 examples/termination/{maxime.fst => Maxime.fst} | 0 examples/termination/{mcCarthy91.fst => McCarthy91.fst} | 0 examples/termination/{termination.fst => Termination.fst} | 0 tests/bug-reports/Bug1347b.fst | 2 +- tests/bug-reports/Makefile | 2 +- tests/bug-reports/{unfold.fst => Unfold.fst} | 0 tests/bug-reports/{unfold.fst.hints => Unfold.fst.hints} | 0 tests/ide/emacs/{backtracking.fst => Backtracking.fst} | 0 ...h-unset-module.in => Backtracking.peek-with-unset-module.in} | 0 ...xpected => Backtracking.peek-with-unset-module.out.expected} | 0 ...{backtracking.refinements.in => Backtracking.refinements.in} | 0 ...ments.out.expected => Backtracking.refinements.out.expected} | 0 tests/ide/emacs/{fstarmode_gh73.fst => FStarMode_GH73.fst} | 0 tests/ide/emacs/{fstarmode_gh73.in => FStarMode_GH73.in} | 0 ...{fstarmode_gh73.out.expected => FStarMode_GH73.out.expected} | 0 tests/ide/emacs/{fib.compute.in => Fib.compute.in} | 0 .../{fib.compute.out.expected => Fib.compute.out.expected} | 0 tests/ide/emacs/{fib.fst => Fib.fst} | 0 tests/ide/emacs/{infotable.fst => InfoTable.fst} | 0 tests/ide/emacs/{infotable.lookup.in => InfoTable.lookup.in} | 0 ...otable.lookup.out.expected => InfoTable.lookup.out.expected} | 0 tests/ide/emacs/{integration.fst => Integration.fst} | 0 .../emacs/{integration.push-pop.in => Integration.push-pop.in} | 0 ....push-pop.out.expected => Integration.push-pop.out.expected} | 0 ...al.autocomplete-global.in => Minimal.autocomplete-global.in} | 0 ...al.out.expected => Minimal.autocomplete-global.out.expected} | 0 ...imal.autocomplete-local.in => Minimal.autocomplete-local.in} | 0 ...cal.out.expected => Minimal.autocomplete-local.out.expected} | 0 tests/ide/emacs/{minimal.compute.in => Minimal.compute.in} | 0 ...inimal.compute.out.expected => Minimal.compute.out.expected} | 0 .../{minimal.describe-repl.in => Minimal.describe-repl.in} | 0 ...ibe-repl.out.expected => Minimal.describe-repl.out.expected} | 0 tests/ide/emacs/{minimal.fst => Minimal.fst} | 0 ...imal.push-no-extra-info.in => Minimal.push-no-extra-info.in} | 0 ...nfo.out.expected => Minimal.push-no-extra-info.out.expected} | 0 tests/ide/emacs/{minimal.push-pop.in => Minimal.push-pop.in} | 0 ...imal.push-pop.out.expected => Minimal.push-pop.out.expected} | 0 ...sitional-location.in => Minimal.push-positional-location.in} | 0 ...t.expected => Minimal.push-positional-location.out.expected} | 0 tests/ide/emacs/{minimal.push.in => Minimal.push.in} | 0 .../{minimal.push.out.expected => Minimal.push.out.expected} | 0 ....unset-current-module.in => Minimal.unset-current-module.in} | 0 ...e.out.expected => Minimal.unset-current-module.out.expected} | 0 tests/ide/emacs/{number.fst => Number.fst} | 0 tests/ide/emacs/{number.fsti => Number.fsti} | 0 ...olation-and-fix.in => Number.interface-violation-and-fix.in} | 0 ...expected => Number.interface-violation-and-fix.out.expected} | 0 ...ber.interface-violation.in => Number.interface-violation.in} | 0 ...ion.out.expected => Number.interface-violation.out.expected} | 0 tests/ide/emacs/{search.cons-snoc.in => Search.cons-snoc.in} | 0 ...rch.cons-snoc.out.expected => Search.cons-snoc.out.expected} | 0 tests/ide/emacs/{search.fst => Search.fst} | 0 tests/ide/emacs/{test.fst => Test.fst} | 0 tests/ide/emacs/{test.fsti => Test.fsti} | 0 tests/ide/emacs/{tutorial.fst => Tutorial.fst} | 0 tests/ide/emacs/{tutorial.push.in => Tutorial.push.in} | 0 .../{tutorial.push.out.expected => Tutorial.push.out.expected} | 0 tests/ide/emacs/{tutorial.segment.in => Tutorial.segment.in} | 0 ...orial.segment.out.expected => Tutorial.segment.out.expected} | 0 tests/micro-benchmarks/{arith.fst => Arith.fst} | 0 tests/micro-benchmarks/{arith.fst.hints => Arith.fst.hints} | 0 tests/micro-benchmarks/{Mac.fst => MAC.fst} | 0 tests/micro-benchmarks/{Mac.fst.hints => MAC.fst.hints} | 0 67 files changed, 3 insertions(+), 3 deletions(-) rename examples/dm4free/{delimcc.fst => DelimCC.fst} (100%) rename examples/metatheory/{indind.fst => IndInd.fst} (99%) rename examples/paradoxes/{propImpredicativeAndNonStrictlyPositiveinductives.fst => PropImpredicativeAndNonStrictlyPositiveInductives.fst} (100%) rename examples/rel/{label.fst => Label.fst} (100%) rename examples/termination/{maxime.fst => Maxime.fst} (100%) rename examples/termination/{mcCarthy91.fst => McCarthy91.fst} (100%) rename examples/termination/{termination.fst => Termination.fst} (100%) rename tests/bug-reports/{unfold.fst => Unfold.fst} (100%) rename tests/bug-reports/{unfold.fst.hints => Unfold.fst.hints} (100%) rename tests/ide/emacs/{backtracking.fst => Backtracking.fst} (100%) rename tests/ide/emacs/{backtracking.peek-with-unset-module.in => Backtracking.peek-with-unset-module.in} (100%) rename tests/ide/emacs/{backtracking.peek-with-unset-module.out.expected => Backtracking.peek-with-unset-module.out.expected} (100%) rename tests/ide/emacs/{backtracking.refinements.in => Backtracking.refinements.in} (100%) rename tests/ide/emacs/{backtracking.refinements.out.expected => Backtracking.refinements.out.expected} (100%) rename tests/ide/emacs/{fstarmode_gh73.fst => FStarMode_GH73.fst} (100%) rename tests/ide/emacs/{fstarmode_gh73.in => FStarMode_GH73.in} (100%) rename tests/ide/emacs/{fstarmode_gh73.out.expected => FStarMode_GH73.out.expected} (100%) rename tests/ide/emacs/{fib.compute.in => Fib.compute.in} (100%) rename tests/ide/emacs/{fib.compute.out.expected => Fib.compute.out.expected} (100%) rename tests/ide/emacs/{fib.fst => Fib.fst} (100%) rename tests/ide/emacs/{infotable.fst => InfoTable.fst} (100%) rename tests/ide/emacs/{infotable.lookup.in => InfoTable.lookup.in} (100%) rename tests/ide/emacs/{infotable.lookup.out.expected => InfoTable.lookup.out.expected} (100%) rename tests/ide/emacs/{integration.fst => Integration.fst} (100%) rename tests/ide/emacs/{integration.push-pop.in => Integration.push-pop.in} (100%) rename tests/ide/emacs/{integration.push-pop.out.expected => Integration.push-pop.out.expected} (100%) rename tests/ide/emacs/{minimal.autocomplete-global.in => Minimal.autocomplete-global.in} (100%) rename tests/ide/emacs/{minimal.autocomplete-global.out.expected => Minimal.autocomplete-global.out.expected} (100%) rename tests/ide/emacs/{minimal.autocomplete-local.in => Minimal.autocomplete-local.in} (100%) rename tests/ide/emacs/{minimal.autocomplete-local.out.expected => Minimal.autocomplete-local.out.expected} (100%) rename tests/ide/emacs/{minimal.compute.in => Minimal.compute.in} (100%) rename tests/ide/emacs/{minimal.compute.out.expected => Minimal.compute.out.expected} (100%) rename tests/ide/emacs/{minimal.describe-repl.in => Minimal.describe-repl.in} (100%) rename tests/ide/emacs/{minimal.describe-repl.out.expected => Minimal.describe-repl.out.expected} (100%) rename tests/ide/emacs/{minimal.fst => Minimal.fst} (100%) rename tests/ide/emacs/{minimal.push-no-extra-info.in => Minimal.push-no-extra-info.in} (100%) rename tests/ide/emacs/{minimal.push-no-extra-info.out.expected => Minimal.push-no-extra-info.out.expected} (100%) rename tests/ide/emacs/{minimal.push-pop.in => Minimal.push-pop.in} (100%) rename tests/ide/emacs/{minimal.push-pop.out.expected => Minimal.push-pop.out.expected} (100%) rename tests/ide/emacs/{minimal.push-positional-location.in => Minimal.push-positional-location.in} (100%) rename tests/ide/emacs/{minimal.push-positional-location.out.expected => Minimal.push-positional-location.out.expected} (100%) rename tests/ide/emacs/{minimal.push.in => Minimal.push.in} (100%) rename tests/ide/emacs/{minimal.push.out.expected => Minimal.push.out.expected} (100%) rename tests/ide/emacs/{minimal.unset-current-module.in => Minimal.unset-current-module.in} (100%) rename tests/ide/emacs/{minimal.unset-current-module.out.expected => Minimal.unset-current-module.out.expected} (100%) rename tests/ide/emacs/{number.fst => Number.fst} (100%) rename tests/ide/emacs/{number.fsti => Number.fsti} (100%) rename tests/ide/emacs/{number.interface-violation-and-fix.in => Number.interface-violation-and-fix.in} (100%) rename tests/ide/emacs/{number.interface-violation-and-fix.out.expected => Number.interface-violation-and-fix.out.expected} (100%) rename tests/ide/emacs/{number.interface-violation.in => Number.interface-violation.in} (100%) rename tests/ide/emacs/{number.interface-violation.out.expected => Number.interface-violation.out.expected} (100%) rename tests/ide/emacs/{search.cons-snoc.in => Search.cons-snoc.in} (100%) rename tests/ide/emacs/{search.cons-snoc.out.expected => Search.cons-snoc.out.expected} (100%) rename tests/ide/emacs/{search.fst => Search.fst} (100%) rename tests/ide/emacs/{test.fst => Test.fst} (100%) rename tests/ide/emacs/{test.fsti => Test.fsti} (100%) rename tests/ide/emacs/{tutorial.fst => Tutorial.fst} (100%) rename tests/ide/emacs/{tutorial.push.in => Tutorial.push.in} (100%) rename tests/ide/emacs/{tutorial.push.out.expected => Tutorial.push.out.expected} (100%) rename tests/ide/emacs/{tutorial.segment.in => Tutorial.segment.in} (100%) rename tests/ide/emacs/{tutorial.segment.out.expected => Tutorial.segment.out.expected} (100%) rename tests/micro-benchmarks/{arith.fst => Arith.fst} (100%) rename tests/micro-benchmarks/{arith.fst.hints => Arith.fst.hints} (100%) rename tests/micro-benchmarks/{Mac.fst => MAC.fst} (100%) rename tests/micro-benchmarks/{Mac.fst.hints => MAC.fst.hints} (100%) diff --git a/examples/dm4free/delimcc.fst b/examples/dm4free/DelimCC.fst similarity index 100% rename from examples/dm4free/delimcc.fst rename to examples/dm4free/DelimCC.fst diff --git a/examples/metatheory/indind.fst b/examples/metatheory/IndInd.fst similarity index 99% rename from examples/metatheory/indind.fst rename to examples/metatheory/IndInd.fst index 0289c487117..dbd3e82523a 100644 --- a/examples/metatheory/indind.fst +++ b/examples/metatheory/IndInd.fst @@ -13,7 +13,7 @@ See the License for the specific language governing permissions and limitations under the License. *) -module Indind +module IndInd /// Induction-induction can be encoded in F* at least up to simple /// elimination (see Forsberg ...) diff --git a/examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst b/examples/paradoxes/PropImpredicativeAndNonStrictlyPositiveInductives.fst similarity index 100% rename from examples/paradoxes/propImpredicativeAndNonStrictlyPositiveinductives.fst rename to examples/paradoxes/PropImpredicativeAndNonStrictlyPositiveInductives.fst diff --git a/examples/rel/label.fst b/examples/rel/Label.fst similarity index 100% rename from examples/rel/label.fst rename to examples/rel/Label.fst diff --git a/examples/termination/maxime.fst b/examples/termination/Maxime.fst similarity index 100% rename from examples/termination/maxime.fst rename to examples/termination/Maxime.fst diff --git a/examples/termination/mcCarthy91.fst b/examples/termination/McCarthy91.fst similarity index 100% rename from examples/termination/mcCarthy91.fst rename to examples/termination/McCarthy91.fst diff --git a/examples/termination/termination.fst b/examples/termination/Termination.fst similarity index 100% rename from examples/termination/termination.fst rename to examples/termination/Termination.fst diff --git a/tests/bug-reports/Bug1347b.fst b/tests/bug-reports/Bug1347b.fst index f99711f42a0..337738d0fb0 100644 --- a/tests/bug-reports/Bug1347b.fst +++ b/tests/bug-reports/Bug1347b.fst @@ -13,7 +13,7 @@ See the License for the specific language governing permissions and limitations under the License. *) -module Bug1347B +module Bug1347b open FStar.Tactics.V2 diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile index ff6c7c0439f..1c5ed101806 100644 --- a/tests/bug-reports/Makefile +++ b/tests/bug-reports/Makefile @@ -35,7 +35,7 @@ SHOULD_VERIFY_CLOSED=\ UnificationCrash.fst Bug1150.fst Bug1076.fst Bug1341.fst Bug1345.fst \ Bug1345b.fst Bug1345c.fst Bug1346.fst Bug1348.fst Bug1362.fst \ Bug1347b.fst Bug1206.fst Bug1271.fst Bug1305.fst Bug1361.fst Bug1383.fst \ - Bug1414.fst unfold.fst Bug1091.fst Bug1449.fst Bug1427.fst Bug1423.fst \ + Bug1414.fst Unfold.fst Bug1091.fst Bug1449.fst Bug1427.fst Bug1423.fst \ Bug1352.fst Bug1123.fst ScopeOfBinderGuard.fst Bug1319a.fst Bug1319b.fst \ Bug1319c.fst Bug1319d.fst Bug1319e.fst Bug1319f.fst Bug807a.fst \ Bug807b.fst Bug807c.fst Bug807d.fst Bug807e.fst Bug1502.fst Bug1488.fst \ diff --git a/tests/bug-reports/unfold.fst b/tests/bug-reports/Unfold.fst similarity index 100% rename from tests/bug-reports/unfold.fst rename to tests/bug-reports/Unfold.fst diff --git a/tests/bug-reports/unfold.fst.hints b/tests/bug-reports/Unfold.fst.hints similarity index 100% rename from tests/bug-reports/unfold.fst.hints rename to tests/bug-reports/Unfold.fst.hints diff --git a/tests/ide/emacs/backtracking.fst b/tests/ide/emacs/Backtracking.fst similarity index 100% rename from tests/ide/emacs/backtracking.fst rename to tests/ide/emacs/Backtracking.fst diff --git a/tests/ide/emacs/backtracking.peek-with-unset-module.in b/tests/ide/emacs/Backtracking.peek-with-unset-module.in similarity index 100% rename from tests/ide/emacs/backtracking.peek-with-unset-module.in rename to tests/ide/emacs/Backtracking.peek-with-unset-module.in diff --git a/tests/ide/emacs/backtracking.peek-with-unset-module.out.expected b/tests/ide/emacs/Backtracking.peek-with-unset-module.out.expected similarity index 100% rename from tests/ide/emacs/backtracking.peek-with-unset-module.out.expected rename to tests/ide/emacs/Backtracking.peek-with-unset-module.out.expected diff --git a/tests/ide/emacs/backtracking.refinements.in b/tests/ide/emacs/Backtracking.refinements.in similarity index 100% rename from tests/ide/emacs/backtracking.refinements.in rename to tests/ide/emacs/Backtracking.refinements.in diff --git a/tests/ide/emacs/backtracking.refinements.out.expected b/tests/ide/emacs/Backtracking.refinements.out.expected similarity index 100% rename from tests/ide/emacs/backtracking.refinements.out.expected rename to tests/ide/emacs/Backtracking.refinements.out.expected diff --git a/tests/ide/emacs/fstarmode_gh73.fst b/tests/ide/emacs/FStarMode_GH73.fst similarity index 100% rename from tests/ide/emacs/fstarmode_gh73.fst rename to tests/ide/emacs/FStarMode_GH73.fst diff --git a/tests/ide/emacs/fstarmode_gh73.in b/tests/ide/emacs/FStarMode_GH73.in similarity index 100% rename from tests/ide/emacs/fstarmode_gh73.in rename to tests/ide/emacs/FStarMode_GH73.in diff --git a/tests/ide/emacs/fstarmode_gh73.out.expected b/tests/ide/emacs/FStarMode_GH73.out.expected similarity index 100% rename from tests/ide/emacs/fstarmode_gh73.out.expected rename to tests/ide/emacs/FStarMode_GH73.out.expected diff --git a/tests/ide/emacs/fib.compute.in b/tests/ide/emacs/Fib.compute.in similarity index 100% rename from tests/ide/emacs/fib.compute.in rename to tests/ide/emacs/Fib.compute.in diff --git a/tests/ide/emacs/fib.compute.out.expected b/tests/ide/emacs/Fib.compute.out.expected similarity index 100% rename from tests/ide/emacs/fib.compute.out.expected rename to tests/ide/emacs/Fib.compute.out.expected diff --git a/tests/ide/emacs/fib.fst b/tests/ide/emacs/Fib.fst similarity index 100% rename from tests/ide/emacs/fib.fst rename to tests/ide/emacs/Fib.fst diff --git a/tests/ide/emacs/infotable.fst b/tests/ide/emacs/InfoTable.fst similarity index 100% rename from tests/ide/emacs/infotable.fst rename to tests/ide/emacs/InfoTable.fst diff --git a/tests/ide/emacs/infotable.lookup.in b/tests/ide/emacs/InfoTable.lookup.in similarity index 100% rename from tests/ide/emacs/infotable.lookup.in rename to tests/ide/emacs/InfoTable.lookup.in diff --git a/tests/ide/emacs/infotable.lookup.out.expected b/tests/ide/emacs/InfoTable.lookup.out.expected similarity index 100% rename from tests/ide/emacs/infotable.lookup.out.expected rename to tests/ide/emacs/InfoTable.lookup.out.expected diff --git a/tests/ide/emacs/integration.fst b/tests/ide/emacs/Integration.fst similarity index 100% rename from tests/ide/emacs/integration.fst rename to tests/ide/emacs/Integration.fst diff --git a/tests/ide/emacs/integration.push-pop.in b/tests/ide/emacs/Integration.push-pop.in similarity index 100% rename from tests/ide/emacs/integration.push-pop.in rename to tests/ide/emacs/Integration.push-pop.in diff --git a/tests/ide/emacs/integration.push-pop.out.expected b/tests/ide/emacs/Integration.push-pop.out.expected similarity index 100% rename from tests/ide/emacs/integration.push-pop.out.expected rename to tests/ide/emacs/Integration.push-pop.out.expected diff --git a/tests/ide/emacs/minimal.autocomplete-global.in b/tests/ide/emacs/Minimal.autocomplete-global.in similarity index 100% rename from tests/ide/emacs/minimal.autocomplete-global.in rename to tests/ide/emacs/Minimal.autocomplete-global.in diff --git a/tests/ide/emacs/minimal.autocomplete-global.out.expected b/tests/ide/emacs/Minimal.autocomplete-global.out.expected similarity index 100% rename from tests/ide/emacs/minimal.autocomplete-global.out.expected rename to tests/ide/emacs/Minimal.autocomplete-global.out.expected diff --git a/tests/ide/emacs/minimal.autocomplete-local.in b/tests/ide/emacs/Minimal.autocomplete-local.in similarity index 100% rename from tests/ide/emacs/minimal.autocomplete-local.in rename to tests/ide/emacs/Minimal.autocomplete-local.in diff --git a/tests/ide/emacs/minimal.autocomplete-local.out.expected b/tests/ide/emacs/Minimal.autocomplete-local.out.expected similarity index 100% rename from tests/ide/emacs/minimal.autocomplete-local.out.expected rename to tests/ide/emacs/Minimal.autocomplete-local.out.expected diff --git a/tests/ide/emacs/minimal.compute.in b/tests/ide/emacs/Minimal.compute.in similarity index 100% rename from tests/ide/emacs/minimal.compute.in rename to tests/ide/emacs/Minimal.compute.in diff --git a/tests/ide/emacs/minimal.compute.out.expected b/tests/ide/emacs/Minimal.compute.out.expected similarity index 100% rename from tests/ide/emacs/minimal.compute.out.expected rename to tests/ide/emacs/Minimal.compute.out.expected diff --git a/tests/ide/emacs/minimal.describe-repl.in b/tests/ide/emacs/Minimal.describe-repl.in similarity index 100% rename from tests/ide/emacs/minimal.describe-repl.in rename to tests/ide/emacs/Minimal.describe-repl.in diff --git a/tests/ide/emacs/minimal.describe-repl.out.expected b/tests/ide/emacs/Minimal.describe-repl.out.expected similarity index 100% rename from tests/ide/emacs/minimal.describe-repl.out.expected rename to tests/ide/emacs/Minimal.describe-repl.out.expected diff --git a/tests/ide/emacs/minimal.fst b/tests/ide/emacs/Minimal.fst similarity index 100% rename from tests/ide/emacs/minimal.fst rename to tests/ide/emacs/Minimal.fst diff --git a/tests/ide/emacs/minimal.push-no-extra-info.in b/tests/ide/emacs/Minimal.push-no-extra-info.in similarity index 100% rename from tests/ide/emacs/minimal.push-no-extra-info.in rename to tests/ide/emacs/Minimal.push-no-extra-info.in diff --git a/tests/ide/emacs/minimal.push-no-extra-info.out.expected b/tests/ide/emacs/Minimal.push-no-extra-info.out.expected similarity index 100% rename from tests/ide/emacs/minimal.push-no-extra-info.out.expected rename to tests/ide/emacs/Minimal.push-no-extra-info.out.expected diff --git a/tests/ide/emacs/minimal.push-pop.in b/tests/ide/emacs/Minimal.push-pop.in similarity index 100% rename from tests/ide/emacs/minimal.push-pop.in rename to tests/ide/emacs/Minimal.push-pop.in diff --git a/tests/ide/emacs/minimal.push-pop.out.expected b/tests/ide/emacs/Minimal.push-pop.out.expected similarity index 100% rename from tests/ide/emacs/minimal.push-pop.out.expected rename to tests/ide/emacs/Minimal.push-pop.out.expected diff --git a/tests/ide/emacs/minimal.push-positional-location.in b/tests/ide/emacs/Minimal.push-positional-location.in similarity index 100% rename from tests/ide/emacs/minimal.push-positional-location.in rename to tests/ide/emacs/Minimal.push-positional-location.in diff --git a/tests/ide/emacs/minimal.push-positional-location.out.expected b/tests/ide/emacs/Minimal.push-positional-location.out.expected similarity index 100% rename from tests/ide/emacs/minimal.push-positional-location.out.expected rename to tests/ide/emacs/Minimal.push-positional-location.out.expected diff --git a/tests/ide/emacs/minimal.push.in b/tests/ide/emacs/Minimal.push.in similarity index 100% rename from tests/ide/emacs/minimal.push.in rename to tests/ide/emacs/Minimal.push.in diff --git a/tests/ide/emacs/minimal.push.out.expected b/tests/ide/emacs/Minimal.push.out.expected similarity index 100% rename from tests/ide/emacs/minimal.push.out.expected rename to tests/ide/emacs/Minimal.push.out.expected diff --git a/tests/ide/emacs/minimal.unset-current-module.in b/tests/ide/emacs/Minimal.unset-current-module.in similarity index 100% rename from tests/ide/emacs/minimal.unset-current-module.in rename to tests/ide/emacs/Minimal.unset-current-module.in diff --git a/tests/ide/emacs/minimal.unset-current-module.out.expected b/tests/ide/emacs/Minimal.unset-current-module.out.expected similarity index 100% rename from tests/ide/emacs/minimal.unset-current-module.out.expected rename to tests/ide/emacs/Minimal.unset-current-module.out.expected diff --git a/tests/ide/emacs/number.fst b/tests/ide/emacs/Number.fst similarity index 100% rename from tests/ide/emacs/number.fst rename to tests/ide/emacs/Number.fst diff --git a/tests/ide/emacs/number.fsti b/tests/ide/emacs/Number.fsti similarity index 100% rename from tests/ide/emacs/number.fsti rename to tests/ide/emacs/Number.fsti diff --git a/tests/ide/emacs/number.interface-violation-and-fix.in b/tests/ide/emacs/Number.interface-violation-and-fix.in similarity index 100% rename from tests/ide/emacs/number.interface-violation-and-fix.in rename to tests/ide/emacs/Number.interface-violation-and-fix.in diff --git a/tests/ide/emacs/number.interface-violation-and-fix.out.expected b/tests/ide/emacs/Number.interface-violation-and-fix.out.expected similarity index 100% rename from tests/ide/emacs/number.interface-violation-and-fix.out.expected rename to tests/ide/emacs/Number.interface-violation-and-fix.out.expected diff --git a/tests/ide/emacs/number.interface-violation.in b/tests/ide/emacs/Number.interface-violation.in similarity index 100% rename from tests/ide/emacs/number.interface-violation.in rename to tests/ide/emacs/Number.interface-violation.in diff --git a/tests/ide/emacs/number.interface-violation.out.expected b/tests/ide/emacs/Number.interface-violation.out.expected similarity index 100% rename from tests/ide/emacs/number.interface-violation.out.expected rename to tests/ide/emacs/Number.interface-violation.out.expected diff --git a/tests/ide/emacs/search.cons-snoc.in b/tests/ide/emacs/Search.cons-snoc.in similarity index 100% rename from tests/ide/emacs/search.cons-snoc.in rename to tests/ide/emacs/Search.cons-snoc.in diff --git a/tests/ide/emacs/search.cons-snoc.out.expected b/tests/ide/emacs/Search.cons-snoc.out.expected similarity index 100% rename from tests/ide/emacs/search.cons-snoc.out.expected rename to tests/ide/emacs/Search.cons-snoc.out.expected diff --git a/tests/ide/emacs/search.fst b/tests/ide/emacs/Search.fst similarity index 100% rename from tests/ide/emacs/search.fst rename to tests/ide/emacs/Search.fst diff --git a/tests/ide/emacs/test.fst b/tests/ide/emacs/Test.fst similarity index 100% rename from tests/ide/emacs/test.fst rename to tests/ide/emacs/Test.fst diff --git a/tests/ide/emacs/test.fsti b/tests/ide/emacs/Test.fsti similarity index 100% rename from tests/ide/emacs/test.fsti rename to tests/ide/emacs/Test.fsti diff --git a/tests/ide/emacs/tutorial.fst b/tests/ide/emacs/Tutorial.fst similarity index 100% rename from tests/ide/emacs/tutorial.fst rename to tests/ide/emacs/Tutorial.fst diff --git a/tests/ide/emacs/tutorial.push.in b/tests/ide/emacs/Tutorial.push.in similarity index 100% rename from tests/ide/emacs/tutorial.push.in rename to tests/ide/emacs/Tutorial.push.in diff --git a/tests/ide/emacs/tutorial.push.out.expected b/tests/ide/emacs/Tutorial.push.out.expected similarity index 100% rename from tests/ide/emacs/tutorial.push.out.expected rename to tests/ide/emacs/Tutorial.push.out.expected diff --git a/tests/ide/emacs/tutorial.segment.in b/tests/ide/emacs/Tutorial.segment.in similarity index 100% rename from tests/ide/emacs/tutorial.segment.in rename to tests/ide/emacs/Tutorial.segment.in diff --git a/tests/ide/emacs/tutorial.segment.out.expected b/tests/ide/emacs/Tutorial.segment.out.expected similarity index 100% rename from tests/ide/emacs/tutorial.segment.out.expected rename to tests/ide/emacs/Tutorial.segment.out.expected diff --git a/tests/micro-benchmarks/arith.fst b/tests/micro-benchmarks/Arith.fst similarity index 100% rename from tests/micro-benchmarks/arith.fst rename to tests/micro-benchmarks/Arith.fst diff --git a/tests/micro-benchmarks/arith.fst.hints b/tests/micro-benchmarks/Arith.fst.hints similarity index 100% rename from tests/micro-benchmarks/arith.fst.hints rename to tests/micro-benchmarks/Arith.fst.hints diff --git a/tests/micro-benchmarks/Mac.fst b/tests/micro-benchmarks/MAC.fst similarity index 100% rename from tests/micro-benchmarks/Mac.fst rename to tests/micro-benchmarks/MAC.fst diff --git a/tests/micro-benchmarks/Mac.fst.hints b/tests/micro-benchmarks/MAC.fst.hints similarity index 100% rename from tests/micro-benchmarks/Mac.fst.hints rename to tests/micro-benchmarks/MAC.fst.hints From 62bdb9d5a5031c41c58c15ed9c9f46d9c28da5a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 15 Sep 2024 10:26:52 -0700 Subject: [PATCH 3/4] Update expected output One test (Number.interface-violation-and-fix) now actually behaves as it should and considers the fsti. Update it to actually be a "fix" --- tests/ide/emacs/Number.interface-violation-and-fix.in | 2 +- tests/ide/emacs/Number.interface-violation-and-fix.out.expected | 2 +- tests/ide/emacs/Number.interface-violation.out.expected | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/ide/emacs/Number.interface-violation-and-fix.in b/tests/ide/emacs/Number.interface-violation-and-fix.in index 43584044e33..70b111ccee8 100644 --- a/tests/ide/emacs/Number.interface-violation-and-fix.in +++ b/tests/ide/emacs/Number.interface-violation-and-fix.in @@ -4,4 +4,4 @@ {"query-id":"4","query":"pop","args":{}} {"query-id":"5","query":"vfs-add","args":{"filename":"number.fsti","contents":"module Number\n\nval a : a:int{a < 0}\n"}} {"query-id":"6","query":"push","args":{"kind":"full","code":"module Number\n","line":1,"column":0}} -{"query-id":"7","query":"push","args":{"kind":"full","code":"\nlet a = -1\n","line":2,"column":0}} +{"query-id":"7","query":"push","args":{"kind":"full","code":"\nlet a = 1\n","line":2,"column":0}} diff --git a/tests/ide/emacs/Number.interface-violation-and-fix.out.expected b/tests/ide/emacs/Number.interface-violation-and-fix.out.expected index e2823b698d2..6d74974576f 100644 --- a/tests/ide/emacs/Number.interface-violation-and-fix.out.expected +++ b/tests/ide/emacs/Number.interface-violation-and-fix.out.expected @@ -1,7 +1,7 @@ {"kind": "protocol-info", "rest": "[...]"} {"kind": "response", "query-id": "1", "response": null, "status": "success"} {"kind": "response", "query-id": "2", "response": [], "status": "success"} -{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"} +{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "Number.fsti"}]}], "status": "failure"} {"kind": "response", "query-id": "4", "response": null, "status": "success"} {"kind": "response", "query-id": "5", "response": null, "status": "success"} {"kind": "response", "query-id": "6", "response": [], "status": "success"} diff --git a/tests/ide/emacs/Number.interface-violation.out.expected b/tests/ide/emacs/Number.interface-violation.out.expected index 59c46faba85..1f5309d9a3b 100644 --- a/tests/ide/emacs/Number.interface-violation.out.expected +++ b/tests/ide/emacs/Number.interface-violation.out.expected @@ -1,4 +1,4 @@ {"kind": "protocol-info", "rest": "[...]"} {"kind": "response", "query-id": "1", "response": null, "status": "success"} {"kind": "response", "query-id": "2", "response": [], "status": "success"} -{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"} +{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": ""}, {"beg": [18, 14], "end": [18, 19], "fname": "Number.fsti"}]}], "status": "failure"} From cadd28e52cbe7e9d574bc8ff6e27f631aa4c403c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 15 Sep 2024 13:22:39 -0700 Subject: [PATCH 4/4] snap --- ocaml/fstar-lib/generated/FStar_Parser_Dep.ml | 29 ++++++++++++------- ocaml/fstar-lib/generated/FStar_Universal.ml | 11 ++++++- 2 files changed, 28 insertions(+), 12 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index 40bb2021e55..2e7a26b4388 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -910,16 +910,18 @@ let (check_module_declaration_against_filename : FStar_Ident.lident -> Prims.string -> unit) = fun lid -> fun filename -> - let k' = lowercase_join_longident lid true in + let k' = string_of_lid lid true in let uu___ = - let uu___1 = - let uu___2 = - let uu___3 = - let uu___4 = FStar_Compiler_Util.basename filename in - check_and_strip_suffix uu___4 in - FStar_Compiler_Util.must uu___3 in - FStar_Compiler_String.lowercase uu___2 in - uu___1 <> k' in + (let uu___1 = + let uu___2 = + let uu___3 = FStar_Compiler_Util.basename filename in + check_and_strip_suffix uu___3 in + FStar_Compiler_Util.must uu___2 in + uu___1 <> k') && + (let uu___1 = + let uu___2 = FStar_Compiler_Util.basename filename in + uu___2 = "prims.fst" in + Prims.op_Negation uu___1) in if uu___ then let uu___1 = @@ -927,10 +929,15 @@ let (check_module_declaration_against_filename : let uu___3 = let uu___4 = string_of_lid lid true in FStar_Compiler_Util.format2 - "The module declaration \"module %s\" found in file %s does not match its filename. Dependencies will be incorrect and the module will not be verified." + "The module declaration \"module %s\" found in file %s does not match its filename." uu___4 filename in FStar_Errors_Msg.text uu___3 in - [uu___2] in + let uu___3 = + let uu___4 = + FStar_Errors_Msg.text + "Dependencies will be incorrect and the module will not be verified." in + [uu___4] in + uu___2 :: uu___3 in FStar_Errors.log_issue FStar_Ident.hasrange_lident lid FStar_Errors_Codes.Error_ModuleFileNameMismatch () (Obj.magic FStar_Errors_Msg.is_error_message_list_doc) diff --git a/ocaml/fstar-lib/generated/FStar_Universal.ml b/ocaml/fstar-lib/generated/FStar_Universal.ml index 7d94dd1b872..8eb8fe94bb9 100644 --- a/ocaml/fstar-lib/generated/FStar_Universal.ml +++ b/ocaml/fstar-lib/generated/FStar_Universal.ml @@ -203,13 +203,22 @@ let (parse : FStar_ToSyntax_Interleave.interleave_module ast true in with_dsenv_of_env env1 uu___8) + | (FStar_Parser_AST.Interface (lid1, uu___5, uu___6), + FStar_Parser_AST.Module (lid2, uu___7)) -> + FStar_Errors.raise_error + FStar_Ident.hasrange_lident lid1 + FStar_Errors_Codes.Fatal_PreModuleMismatch () + (Obj.magic + FStar_Errors_Msg.is_error_message_string) + (Obj.magic + "Module name in implementation does not match that of interface.") | uu___5 -> FStar_Errors.raise_error0 FStar_Errors_Codes.Fatal_PreModuleMismatch () (Obj.magic FStar_Errors_Msg.is_error_message_string) (Obj.magic - "mismatch between pre-module and module"))) in + "Module name in implementation does not match that of interface."))) in (match uu___2 with | (ast1, env1) -> let uu___3 = FStar_ToSyntax_ToSyntax.ast_modul_to_modul ast1 in