From 58d19b80b9bfbcdceeac2f47a7a7e2ddc29fdd7d Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 11 Aug 2023 16:56:03 +1000 Subject: [PATCH] test: compiling from the interpreter, with common imports hacky fix to windows test Include test from #2407 as well --- tests/pkg/frontend/Frontend.lean | 3 ++ tests/pkg/frontend/Frontend/Compile.lean | 28 ++++++++++++++++ tests/pkg/frontend/Frontend/Import1.lean | 1 + tests/pkg/frontend/Frontend/Import2.lean | 1 + tests/pkg/frontend/Frontend/Main.lean | 13 ++++++++ .../frontend/Frontend/Main_with_Import2.lean | 2 ++ .../Frontend/Main_with_Import2_and_eval.lean | 6 ++++ .../pkg/frontend/Frontend/Main_with_eval.lean | 5 +++ .../pkg/frontend/Frontend/RegisterOption.lean | 6 ++++ tests/pkg/frontend/lakefile.lean | 17 ++++++++++ tests/pkg/frontend/test.sh | 32 +++++++++++++++++++ 11 files changed, 114 insertions(+) create mode 100644 tests/pkg/frontend/Frontend.lean create mode 100644 tests/pkg/frontend/Frontend/Compile.lean create mode 100644 tests/pkg/frontend/Frontend/Import1.lean create mode 100644 tests/pkg/frontend/Frontend/Import2.lean create mode 100644 tests/pkg/frontend/Frontend/Main.lean create mode 100644 tests/pkg/frontend/Frontend/Main_with_Import2.lean create mode 100644 tests/pkg/frontend/Frontend/Main_with_Import2_and_eval.lean create mode 100644 tests/pkg/frontend/Frontend/Main_with_eval.lean create mode 100644 tests/pkg/frontend/Frontend/RegisterOption.lean create mode 100644 tests/pkg/frontend/lakefile.lean create mode 100755 tests/pkg/frontend/test.sh diff --git a/tests/pkg/frontend/Frontend.lean b/tests/pkg/frontend/Frontend.lean new file mode 100644 index 0000000000..211aebc82b --- /dev/null +++ b/tests/pkg/frontend/Frontend.lean @@ -0,0 +1,3 @@ +import Frontend.RegisterOption +import Frontend.Import1 +import Frontend.Import2 diff --git a/tests/pkg/frontend/Frontend/Compile.lean b/tests/pkg/frontend/Frontend/Compile.lean new file mode 100644 index 0000000000..165d4e3b06 --- /dev/null +++ b/tests/pkg/frontend/Frontend/Compile.lean @@ -0,0 +1,28 @@ +import Lean.Elab.Frontend + +open Lean Elab + +unsafe def processInput (input : String) (initializers := false) : + IO (Environment × List Message) := do + let fileName := "" + let inputCtx := Parser.mkInputContext input fileName + if initializers then enableInitializersExecution + let (header, parserState, messages) ← Parser.parseHeader inputCtx + let (env, messages) ← processHeader header {} messages inputCtx + let s ← IO.processCommands inputCtx parserState (Command.mkState env messages {}) <&> Frontend.State.commandState + pure (s.env, s.messages.msgs.toList) + +open System in +def findLean (mod : Name) : IO FilePath := do + let olean ← findOLean mod + -- Remove a "build/lib/" substring from the path. + let lean := olean.toString.replace (toString (FilePath.mk "build" / "lib") ++ FilePath.pathSeparator.toString) "" + return FilePath.mk lean |>.withExtension "lean" + +/-- Read the source code of the named module. -/ +def moduleSource (mod : Name) : IO String := do + IO.FS.readFile (← findLean mod) + +unsafe def compileModule (mod : Name) (initializers := false) : + IO (Environment × List Message) := do + processInput (← moduleSource mod) initializers diff --git a/tests/pkg/frontend/Frontend/Import1.lean b/tests/pkg/frontend/Frontend/Import1.lean new file mode 100644 index 0000000000..605cc36883 --- /dev/null +++ b/tests/pkg/frontend/Frontend/Import1.lean @@ -0,0 +1 @@ +import Frontend.RegisterOption diff --git a/tests/pkg/frontend/Frontend/Import2.lean b/tests/pkg/frontend/Frontend/Import2.lean new file mode 100644 index 0000000000..605cc36883 --- /dev/null +++ b/tests/pkg/frontend/Frontend/Import2.lean @@ -0,0 +1 @@ +import Frontend.RegisterOption diff --git a/tests/pkg/frontend/Frontend/Main.lean b/tests/pkg/frontend/Frontend/Main.lean new file mode 100644 index 0000000000..2a4f622de8 --- /dev/null +++ b/tests/pkg/frontend/Frontend/Main.lean @@ -0,0 +1,13 @@ +import Frontend.Compile + +open Lean + +unsafe def main (args : List String) : IO UInt32 := do + initSearchPath (← findSysroot) + let mut count : UInt32 := 0 + for mod in args do + IO.println s!"Compiling {mod}" + let (_env, msgs) ← compileModule mod.toName true + for m in msgs do IO.println (← m.toString) + if msgs.length > 0 then count := 1 + return count diff --git a/tests/pkg/frontend/Frontend/Main_with_Import2.lean b/tests/pkg/frontend/Frontend/Main_with_Import2.lean new file mode 100644 index 0000000000..c806906421 --- /dev/null +++ b/tests/pkg/frontend/Frontend/Main_with_Import2.lean @@ -0,0 +1,2 @@ +import Frontend.Main +import Frontend.Import2 diff --git a/tests/pkg/frontend/Frontend/Main_with_Import2_and_eval.lean b/tests/pkg/frontend/Frontend/Main_with_Import2_and_eval.lean new file mode 100644 index 0000000000..443c336820 --- /dev/null +++ b/tests/pkg/frontend/Frontend/Main_with_Import2_and_eval.lean @@ -0,0 +1,6 @@ +import Frontend.Main +import Frontend.Import2 + +#eval show IO _ from do + let r ← main ["Frontend.Import1"] + if r ≠ 0 then throw <| IO.userError "Messages were generated!" diff --git a/tests/pkg/frontend/Frontend/Main_with_eval.lean b/tests/pkg/frontend/Frontend/Main_with_eval.lean new file mode 100644 index 0000000000..37c7e32d7c --- /dev/null +++ b/tests/pkg/frontend/Frontend/Main_with_eval.lean @@ -0,0 +1,5 @@ +import Frontend.Main + +#eval show IO _ from do + let r ← main ["Frontend.Import1"] + if r ≠ 0 then throw <| IO.userError "Messages were generated!" diff --git a/tests/pkg/frontend/Frontend/RegisterOption.lean b/tests/pkg/frontend/Frontend/RegisterOption.lean new file mode 100644 index 0000000000..8ec038226f --- /dev/null +++ b/tests/pkg/frontend/Frontend/RegisterOption.lean @@ -0,0 +1,6 @@ +import Lean + +register_option option : Bool := { + defValue := true + descr := "" +} diff --git a/tests/pkg/frontend/lakefile.lean b/tests/pkg/frontend/lakefile.lean new file mode 100644 index 0000000000..96c88a7305 --- /dev/null +++ b/tests/pkg/frontend/lakefile.lean @@ -0,0 +1,17 @@ +import Lake +open Lake DSL + +package frontend + +@[default_target] +lean_lib Frontend + +lean_exe frontend_with_import2 { + root := `Frontend.Main_with_Import2 + supportInterpreter := true +} + +lean_exe frontend { + root := `Frontend.Main + supportInterpreter := true +} diff --git a/tests/pkg/frontend/test.sh b/tests/pkg/frontend/test.sh new file mode 100755 index 0000000000..b5136d180b --- /dev/null +++ b/tests/pkg/frontend/test.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +rm -rf build +lake build + +# Check that we can compile a file which shares with the executable +# a common import using an initializer. +# Here the executable for `frontend_with_import1` imports `Frontend.Import2`. + +# This is a minimisation of a situation in which we want to compile a file +# from a project (e.g. Mathlib), so that we can inject another tactic +# implemented in the same project into a goal state from the file. + +# This already worked prior to lean4#2423. +lake exe frontend_with_import2 Frontend.Import1 && + +# Check that if we don't import `Frontend.Import2`, we can successfully run +# #eval main ["Frontend.Import1"] +# in the interpreter + +# This already worked prior to lean4#2423. +lake build Frontend.Main_with_eval && + +# However if `Main` has imported `Frontend.Import2`, then +# #eval main ["Frontend.Import1"] +# fails to compile `Frontend.Import1` in the interpreter +# prior to lean4#2423. +lake build Frontend.Main_with_Import2_and_eval && + +# Compiling multiple files with a shared import with an initializer +# failed prior to lean4#2423: +lake exe frontend Frontend.Import1 Frontend.Import2