[Question] About Data Compile

hideonbushhhhhhh commented 2 months ago

Thank you very much for your awesome work! I can't compile the lean code with this repo (https://github.com/rookie-joe/automatic-lean4-compilation), I'd like to know the libraries need to be imported the correct version of lean for which you provide data. Looking forward to your reply very much!

rookie-joe commented 2 months ago

We here attached the lake-manifest.json file, which includes all the necessary information regarding the required libraries and their respective versions.

{"version": 7,
 "packagesDir": ".lake/packages",
 "packages":
 [{"url": "https://github.com/leanprover/std4",
   "type": "git",
   "subDir": null,
   "rev": "e5306c3b0edefe722370b7387ee9bcd4631d6c17",
   "name": "std",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/quote4",
   "type": "git",
   "subDir": null,
   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
   "name": "Qq",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/aesop",
   "type": "git",
   "subDir": null,
   "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9",
   "name": "aesop",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/ProofWidgets4",
   "type": "git",
   "subDir": null,
   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
   "name": "proofwidgets",
   "manifestFile": "lake-manifest.json",
   "inputRev": "v0.0.30",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover/lean4-cli",
   "type": "git",
   "subDir": null,
   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
   "name": "Cli",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/import-graph.git",
   "type": "git",
   "subDir": null,
   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
   "name": "importGraph",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/mathlib4",
   "type": "git",
   "subDir": null,
   "rev": "3cecb823a74ed737c6ebc115e515eba649ec7715",
   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
   "inputRev": "3cecb823a74ed737c6ebc115e515eba649ec7715",
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "REPL",
 "lakeDir": ".lake"}

Please let us know if you have any further questions ;).

hideonbushhhhhhh commented 2 months ago

Thank you for your reply. However, I used REPL to check the correctness of the data, and still found many cases of compilation failure. This is not due to errors in the data, it is because the dataset does not include certain import headers or variables. Perhaps you could provide data that includes these headers? For example:

 theorem erase_toFinmap (a : α) (s : AList β) :
  erase a ⟦s⟧ = AList.toFinmap (s.erase a) := by
   simp [erase]

{"tactics":
 [{"tactic": "simp [erase]",
   "proofState": 0,
   "pos": {"line": 1379, "column": 3},
   "goals":
   "α : Sort u_1\nx✝¹ : Sort u_2\nAList : x✝¹\nx✝ : Sort u_3\nerase : x✝\na : α\ns : sorryAx (Sort u_4) true\n⊢ sorryAx (?m.715 a s) true = sorryAx (?m.715 a s) true",
   "endPos": {"line": 1379, "column": 15}}],
 "messages":
 [{"severity": "error",
   "pos": {"line": 1377, "column": 37},
   "endPos": {"line": 1377, "column": 44},
   "data": "function expected at\n  AList\nterm has type\n  ?m.9"},
  {"severity": "error",
   "pos": {"line": 1378, "column": 2},
   "endPos": {"line": 1378, "column": 13},
   "data": "function expected at\n  erase\nterm has type\n  ?m.19"},
  {"severity": "error",
   "pos": {"line": 1378, "column": 16},
   "endPos": {"line": 1378, "column": 42},
   "data":
   "invalid field notation, type is not of the form (C ...) where C is a constant\n  AList\nhas type\n  ?m.9"},
  {"severity": "error",
   "pos": {"line": 1379, "column": 3},
   "endPos": {"line": 1379, "column": 15},
   "data":
   "invalid argument, variable is not a proposition or let-declaration"}],
 "env": 0}

mriche-saifh commented 2 months ago

Same situation for me. I have been trying to use the FORMAL4 and the OBT datasets. Using the REPL to compile the theorems in these datasets, but most theorem fail at compilation.

I am new to Lean, so it may be just be from my side.

To try solving the missing import headers, I tried the solution suggested in this community discussion, using

import Mathlib
[code]
#min_imports

But that's not enough to have the compilations working.

I guess, I should also use automatic-lean4-compilation instead of REPL, that should help with solving the differences in Mathlib version between REPL and FORMAL4.

rookie-joe commented 2 months ago

Same situation for me. I have been trying to use the FORMAL4 and the OBT datasets. Using the REPL to compile the theorems in these datasets, but most theorem fail at compilation.

I am new to Lean, so it may be just be from my side.

To try solving the missing import headers, I tried the solution suggested in this community discussion, using
import Mathlib
[code]
#min_imports
But that's not enough to have the compilations working.

I guess, I should also use automatic-lean4-compilation instead of REPL, that should help with solving the differences in Mathlib version between REPL and FORMAL4.

Yes, if you directly use the REPL, you will need to revise the lake-manifest and lakefile to include necessary dependencies like mathlib and others.

I kindly suggest using automatic-lean4-compilation, which simplifies the setup process. By following the guidelines in the README, you can easily obtain all the required prerequisites. The community's suggestion is correct: you need to import mathlib for notations, theorems, and more. After installation, you can simply write import Mathlib in your .lean file to start using it.

rookie-joe commented 2 months ago

Thank you for your reply. However, I used REPL to check the correctness of the data, and still found many cases of compilation failure. This is not due to errors in the data, it is because the dataset does not include certain import headers or variables. Perhaps you could provide data that includes these headers? For example:

 theorem erase_toFinmap (a : α) (s : AList β) :
  erase a ⟦s⟧ = AList.toFinmap (s.erase a) := by
   simp [erase]

{"tactics":
 [{"tactic": "simp [erase]",
   "proofState": 0,
   "pos": {"line": 1379, "column": 3},
   "goals":
   "α : Sort u_1\nx✝¹ : Sort u_2\nAList : x✝¹\nx✝ : Sort u_3\nerase : x✝\na : α\ns : sorryAx (Sort u_4) true\n⊢ sorryAx (?m.715 a s) true = sorryAx (?m.715 a s) true",
   "endPos": {"line": 1379, "column": 15}}],
 "messages":
 [{"severity": "error",
   "pos": {"line": 1377, "column": 37},
   "endPos": {"line": 1377, "column": 44},
   "data": "function expected at\n  AList\nterm has type\n  ?m.9"},
  {"severity": "error",
   "pos": {"line": 1378, "column": 2},
   "endPos": {"line": 1378, "column": 13},
   "data": "function expected at\n  erase\nterm has type\n  ?m.19"},
  {"severity": "error",
   "pos": {"line": 1378, "column": 16},
   "endPos": {"line": 1378, "column": 42},
   "data":
   "invalid field notation, type is not of the form (C ...) where C is a constant\n  AList\nhas type\n  ?m.9"},
  {"severity": "error",
   "pos": {"line": 1379, "column": 3},
   "endPos": {"line": 1379, "column": 15},
   "data":
   "invalid argument, variable is not a proposition or let-declaration"}],
 "env": 0}

The errors you're seeing don't necessarily indicate that your theorem is incorrect. Instead, they suggest that certain functions or lemmas required by your theorem are missing from your current environment. For example:

The function erase, which your theorem relies on, is not recognized because it hasn't been defined or imported in your environment.
The error messages indicate that there are missing components (AList, toFinmap, etc.) that are crucial for the successful compilation of your theorem.

Fixing the Compilation Error: The quickest way to resolve this is to ensure that all the necessary definitions (like the erase function and AList.toFinmap) are included before attempting to compile your theorem.

Specifically, if you refer to the Mathlib/Data/Finmap.lean file at this commit, you'll find the definition of erase around line 415. This function relies on dependencies like liftOn, which are defined earlier in the same file. The theorem erase_toFinmap, which you're working on, begins around line 420.

To compile your theorem successfully:

Copy the contents of the Mathlib/Data/Finmap.lean file from the start up to where the erase_toFinmap theorem begins (around line 420). This ensures that all necessary functions and lemmas are available for the compilation process.

Once you've included the necessary content, you can compile your theorem. The error messages should help indicate whether the theorem has been successfully proved or if further adjustments are needed.

rookie-joe / PDA

[Question] About Data Compile #1