building 4.35 now requires git checkout for lean4lean
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 45/100
- Issue type
- Feature
- Clarity
- Mostly clear
- Activity status
- Active
- Tech stack
- git
- Domain
- build-system
Research direction
Start by reading the Fedora packaging spec linked in the issue and trace the Lean 4.35 build steps that fetch lean4lean; check whether nanoda or mimalloc also require network access. The issue asks for a build path using source bundled in the tarball or an additional tarball, and possibly an option to disable optional tools. Done means Fedora packages can build without network access; the issue does not identify a source file or test.
Written by the indexing model from the issue text.
Description
I maintain a package of lean4 for Fedora, and normally we don't have network access when building official Fedora packages (though I could workaround it for now if really needed, since it is not an official Fedora yet, though it may be next year).
Can there be a way to bundle the lean4lean source code in the tarball say, or build from an additional tarball?
(Is git also used for nanoda etc?) If these tools are pretty optional perhaps there could also be an option to disable them?
ps Looking at my current packaging, I see I had also disabled mimalloc support for similar reasons.
I am trying an 4.36 RC1 build now just in case things have already improved..
- Dominant language
- Lean
- Stars
- 9.5k
- Forks
- 1k
- Avg merge
- 23h 57m
- Merged PRs (30d)
- 264
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupOpenbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15674 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
question
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
VV01T3K/ResearchCruiseApp#530 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
tdk-landscape/tdk-cli-core#1658 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
hexdoc-dev/hexdoc#109 ·
-
OptimizationCUTEst jobs fail: gfortran not installed on the runnerPossibly taken @ChrisRackauckas-Claude claimed this today. Open
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
SciML/SciMLBenchmarks.jl#1946 · 1 comment ·
Maintainers usually reply within 1 day