-
Notifications
You must be signed in to change notification settings - Fork 5
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Panic exporting #5
Comments
Can you include some information about your versions of lake, lean, and dependencies? This is most likely due to a version mismatch (then we can get to your point about the instructions not being clear). |
Sure thing.
In test folder:
I hope this helps. If not I can also update the lake-manifest, lakefile or lean-toolchain files. |
Here's an example use:
Note that the argument to |
Thanks @digama0. Here is the output from scratch.
I guess once I can get this minimal example fixed I'll try to think about how to export parts of mathlib. |
Lean versions are different in test and lean4export directory. I don't know if that matters.
In lean4export directory
|
Oh, yes |
Alright, here is the output of the commands, I still get the same issue that it appears not to find Test.
So apparently it is looking for the Test directory. Do I need to append the current path to the search path or do I need to compile the Test "module"? Here is the output of some extra info:
In a non-lean folder i get the following output:
I am not sure how I installed lean, probably by installing the vscode extension. Do I need to update lean? |
You need to compile |
Ok cool, this appears to be working. I will try to experiment a bit and see if I can export a theorem. |
Greetings. I've tried to use the export with no avail.
Process to reproduce.
Stacktrace:
I think I am doing something horribly wrong, but I just can't grasp the how to run. I don't know what the input for the cli is. My goal is quite simple, given an input file that contains one or more theorems, export it.
Also it would be awesome if the exported examples in the example folder had some reproducible steps.
Help is much appreciated.
The text was updated successfully, but these errors were encountered: