make distclean, rebuild all

Stream: lean4

[Kayla Thomas]

Is there an equivalent command for this? If I make a breaking change to one of the files in my project, but I'm not certain of all of the places that it might break, is there a standard way to remove all of the compiled files, recompile, and see where the errors are? Or another way to tell?

[Shreyas Srinivas]

Does this option do the kind of project clean you are asking?
image.png

[Kayla Thomas]

I'm not sure it did. I ran the clean project and then the build project, but it didn't report any of the errors that I was expecting.

[Kayla Thomas]

Maybe it needs the All.lean file which I don't have anything in?

[Shreyas Srinivas]

one option might be to nuke ./.lake

[Shreyas Srinivas]

(at least for the most recent toolchain. Earlier it used to be ./build)

[Shreyas Srinivas]

To get errors you need to import the relevant files at the top

[Kayla Thomas]

Do you mean I need the file that includes all of the lean files in the project?

[Shreyas Srinivas]

If you do that and make a change, there will be a vscode notification to rebuild the imports in all downstream files (when you open them). This will show you an error if the upstream file has one.

[Shreyas Srinivas]

to get the errors during a project build, yes

[Kayla Thomas]

ah, ok. Thank you.

[Shreyas Srinivas]

lake starts at the top and only builds what it needs.

[Shreyas Srinivas]

Of course, you can still get per file (+ its imports) errors when you open that file on the infoview.

[Shreyas Srinivas]

It just won't get built by lake build if it is not imported at the top, directly or indirectly.

[Kayla Thomas]

I see. Thank you.

[Kayla Thomas]

What is the current method to update both Lean and MathLib?

[Kayla Thomas]

pthomas@PC:~/Desktop/github/lean4/FOL$ lake --version
Lake version 5.0.0-a62d2fd (Lean version 4.2.0-rc1)
pthomas@PC:~/Desktop/github/lean4/FOL$ elan --version
elan 3.0.0 (cdb40bff5 2023-09-08)
pthomas@PC:~/Desktop/github/lean4/FOL$ elan show
leanprover/lean4:v4.2.0-rc1 (overridden by '/home/pthomas/Desktop/github/lean4/FOL/lean-toolchain')
Lean (version 4.2.0-rc1, commit a62d2fd49796, Release)
pthomas@PC:~/Desktop/github/lean4/FOL$ lake update
error: ./lake-packages/mathlib/lakefile.lean:84:2: error: unexpected identifier; expected 'abbrev', 'add_decl_doc', 'axiom', 'builtin_initialize', 'class', 'custom_data', 'declare_opaque_type', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'extern_lib', 'family_def', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'lean_exe', 'lean_lib', 'library_data', 'library_facet', 'macro', 'macro_rules', 'module_data', 'module_facet', 'notation', 'opaque', 'package', 'package_data', 'package_facet', 'postfix', 'prefix', 'register_builtin_option', 'register_option', 'script', 'structure', 'syntax', 'target', 'target_data', 'theorem' or 'unif_hint'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

[Scott Morrison]

@Kayla Thomas, I don't immediately see what you're doing wrong. Is this a public repo I could check out?

[Kayla Thomas]

https://github.com/pthomas505/FOL

[Scott Morrison]

@Kayla Thomas, please:

• update your lean-toolchain to say leanprover/lean4:v4.3.0-rc2
• run lake update
• verify lake build works
• you probably want to replace the contents of your .gitignore with just /.lake/

[Scott Morrison]

(Often, lake update will update your lean-toolchain automatically, but it is susceptible to changes in the lakefile syntax...)

[Kayla Thomas]

Thank you!

[Kayla Thomas]

I'm not sure if lake build is working or not.

pthomas@PC:~/Desktop/github/lean4/FOL$ lake clean
pthomas@PC:~/Desktop/github/lean4/FOL$ lake update
mathlib: running post-update hooks
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
No files to download
Decompressing 3960 file(s)
unpacked in 58278 ms
pthomas@PC:~/Desktop/github/lean4/FOL$ lake build
[1/2] Building FOL
pthomas@PC:~/Desktop/github/lean4/FOL$ lake build
pthomas@PC:~/Desktop/github/lean4/FOL$

[Ruben Van de Velde]

It worked

[Mac Malone]

@Kayla Thomas One quick note on your repository: You should delete the root lakefile.olean. That was a Lake artifact from previous versions of Lake that was not meant to be committed.

[Kayla Thomas]

@Mac Malone Done. Thank you.