Inconsistent OPAM packaging of rocq-stdlib
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 42/100
- Tipo di issue
- Bug
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Tranquilla
- Ambito
- build-system, release
Direzione di ricerca
Inizia confrontando la pagina del pacchetto OPAM standard con la pagina del pacchetto del repository Rocq collegata nell’issue, concentrandoti sulle relative versioni e sui metadati del pacchetto. Determina se il pacchetto standard può essere aggiornato alla versione 9.1.0 o rimosso, quindi verifica che gli utenti non ricevano più un pacchetto rocq-stdlib obsoleto dal repository OPAM standard.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
There's a rocq-stdlib package in the standard OPAM repository, https://opam.ocaml.org/packages/rocq-stdlib/ , which is stuck at version 9.0.0, and another package in the Rocq repository, https://rocq-prover.org/p/rocq-stdlib/latest, which is at version 9.1.0.
This is unfortunate: Rocq users run into different issues if they use only the standard OPAM repository (and get an old version of the stdlib) or if they also use the Rocq repository (and get a newer version). See https://github.com/AbsInt/CompCert/issues/580 for an example.
Please keep the OPAM repository package https://opam.ocaml.org/packages/rocq-stdlib/ up to date. Or remove it entirely. But don't keep an outdated version there.
- Lingua principale
- Rocq Prover
- Stelle
- 45
- Fork
- 39
- Merge medio
- 1g 13h
- PR unite (30g)
- 3
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di rocq-prover/stdlib
-
incl_dec and NoDup_dec should be Defined and not QedForse di nuovo libera Una pull request per questa issue è stata chiusa senza essere unita. Aperta
Difficoltà 1/5 1-3 ore Idoneità per principianti 65/100
rocq-prover/stdlib#25 ·
-
Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)Forse già presa @hy7pc8gfmf-dotcom l’ha presa 25 giorni fa. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 6/100
rocq-prover/stdlib#315 ·
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)Forse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100
rocq-prover/stdlib#312 ·
-
Maintaining NaryFunctionsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#293 ·
-
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#243 ·
Tutte le issue di rocq-prover/stdlib
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 62/100
leanprover-community/lean4game#589 ·
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 82/100
unocss/unocss#5421 · 1 commento ·
I maintainer di solito rispondono entro 1 giorno
-
follow-up
Difficoltà 2/5 Mezza giornata Idoneità per principianti 62/100
carrick-sh/carrick#1494 ·
I maintainer di solito rispondono entro 1 giorno
-
good first issue infrastructure
Difficoltà 2/5 1-3 ore Idoneità per principianti 66/100
I maintainer di solito rispondono entro 2 giorni
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 85/100
processing/processing4#1592 ·