Improve functionality for newer lean versions #39
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Allows user to specify where to get the lean server rather than using the one bundled with lean-game-maker. Also automatically downlods lean-game-maker as necessary.
These are no longer necessary since the last commit.
Compression takes very long on newer version of mathlib which are very large. Since devmode is presumably meant for local development, (i.e., on the loopback device, which has very high bandwidth), the increased file size should not be a problem.
Closed
This is necessary for newer versions of lean
|
Additional commit is to properly support newer versions of lean, which have a problem with old versions of BrowserFS. This is ported from #38. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This removes the bundled lean servers in favor of downloading newer versions directly from github. Alternatively, the user may also explicitly specify a folder from which to get the lean server (if they wish to use a custom build for example).
Also, this removes compression from the library zipfile when building in devmode. This is done because newer versions of mathlib are quite large and compression takes a long time (on my machine this reduced build times from around 4 minutes to just 45 seconds). Since devmode will usually be for local development using the loopback device for networking, the bandwidth will be quite large and the larger file size shouldn't cause problems (you'll save more time from reduced build times than you'll waste waiting for the network).