search

knowsys / Formale-Systeme-in-LEAN

LEAN4 formalization of the undergraduate lecture "Formale Systeme" at TU Dresden (WIP)
Apache License 2.0
8 stars 0 forks source link

Upgrade to Lean v4.4.0 #17

Closed monsterkrampe closed 9 months ago

monsterkrampe commented 9 months ago

I fixed the version in lean-toolchain now to avoid unpleasant surprises in the future. We should upgrade this somewhat regularly though :)

monsterkrampe commented 9 months ago

@matzemathics feel free to do the fix here :)

mmarx commented 9 months ago

Please run nix fmt as well, or at least update the formatter if you want to use something other than alejandra.

matzemathics commented 9 months ago

@mmarx any ideas what might be wrong in the nix build? It seems to me as if the lean flake is broken 😕.

mmarx commented 9 months ago

I'll take a look.

mmarx commented 9 months ago

@mmarx any ideas what might be wrong in the nix build? It seems to me as if the lean flake is broken 😕.

The problem is that ProofWidgets4 fails to build, because it has some custom logic in its lakefile.lean that builds Javascript from Typescript. buildLeanPackage doesn't do this, so it fails when the code tries to include those non-existing Javascript files. Not sure what the easy way to fix this would be, though.

monsterkrampe commented 9 months ago

Will merge without the nix changes for now and create a new draft PR for them.