Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Add manifest fetch script #5

Closed
lenianiva opened this issue Oct 26, 2024 · 2 comments · May be fixed by #19
Closed

Add manifest fetch script #5

lenianiva opened this issue Oct 26, 2024 · 2 comments · May be fixed by #19
Assignees
@lenianiva
Labels
feature New feature or request part/manifest Manifest files

Comments

@lenianiva
Copy link
Owner

Manually writing each one is too time consuming. We can support every rc and major version. Otherwise the size of the repository may become too large.
@lenianiva lenianiva self-assigned this Oct 26, 2024
@lenianiva lenianiva added feature New feature or request part/overlay Overlay and toolchain reading part/manifest Manifest files and removed part/overlay Overlay and toolchain reading labels Oct 26, 2024
wuyoli added a commit to wuyoli/lean4-nix that referenced this issue Oct 30, 2024
@wuyoli
feat: manifest fetch script
65cac43 
closes lenianiva#5
@wuyoli wuyoli mentioned this issue Oct 30, 2024
Draft
@lenianiva
Copy link
Owner Author

Since we save a snapshot of each version's bootstrap function, I don't think there is a simple solution for this any time soon unless we ship Lean binary.

@stepbrobd stepbrobd mentioned this issue Nov 7, 2024
Closed
@lenianiva
Copy link
Owner Author

I don't think this is doable given that each manifest has a custom build script and we need to manually fix the script so it builds on MacOS.

@lenianiva lenianiva closed this as not planned Won't fix, can't repro, duplicate, stale Nov 16, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@lenianiva lenianiva

Labels
feature New feature or request part/manifest Manifest files
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

feat: manifest fetch script wuyoli/lean4-nix
1 participant
@lenianiva