Kha
commented
7 years ago Electrolysis is using Lean 2, I should probably mention that in the readme. Porting it to Lean 3 would not be a small endeavor, and so will probably not happen anytime in the near future because I'm focused on other projects at the moment. Having said that, the project would certainly benefit from Lean 3's metaprogramming and better automation.
arademaker
I am using Lean version 3.2.1, but can't seem to sort out the imports and opens.
For example, inside core/generated.lean, at the first line, I get the error "file 'core/pre' not found in the LEAN_PATH. I can fix this particular error by changing the import to read import ..core.pre. Is there another way to fix this that doesn't involve editing the files?
In sem.lean, at line 3, open eq.ops, I get the error "invalid namespace name 'eq.ops'". Is replacing that line with open eq OK?
Finally, anywhere where there is an command of the form open [.+] .+ I get the error "invalid 'open/export' command, identifier expected". I am not sure how to fix those either.
I suspect that this could all be fixed by switching to the correct Lean version. What version of Lean does electrolysis depend on? Is there a fix that doesn't involve switching versions of Lean?
Thanks!