Bottlenecks in standard library
I maintainer di solito rispondono entro 2 giorni
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 35/100
- Tipo di issue
- Refactoring
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- build-system
Direzione di ricerca
Inizia esaminando le istruzioni Require Export in Reals/Ranalysis.v e il Require Import in Reals/NewtonInt.v, inclusa la dipendenza da Rgeom. Determina quali importazioni sono effettivamente necessarie per i file della libreria standard, quindi verifica che la rimozione delle dipendenze non necessarie riduca i colli di bottiglia della compilazione parallela.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
Description of the problem
The standard library contains files such as Reals/Ranalysis.v, which mainly contain Require Export xyz.
This is great for users (no need to search the exact file names). However, when used in the standard library internally, this creates a bottleneck with respect to parallel compilation of the standard library.
For example, Reals/NewtonInt.v contains Require Import Ranalysis., which (among others) exports Rgeom.
However, Rgeom is not necessary for NewtonInt. Still in parallel compilation NewtonInt needs Rgeom to compile first.
Avoiding unnecessary bottlenecks by better import management in the standard library may improve parallel compilation speed.
Coq Version
8.17
- Lingua principale
- Rocq Prover
- Stelle
- 43
- Fork
- 39
- Merge medio
- 4g 13h
- PR unite (30g)
- 6
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 ·
I maintainer di solito rispondono entro 2 giorni
-
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 18 giorni fa. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 6/100
rocq-prover/stdlib#315 ·
I maintainer di solito rispondono entro 2 giorni
-
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 ·
I maintainer di solito rispondono entro 2 giorni
-
Maintaining NaryFunctionsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#293 ·
I maintainer di solito rispondono entro 2 giorni
-
Inconsistent OPAM packaging of rocq-stdlibForse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100
rocq-prover/stdlib#256 · 4 commenti · 3 reazioni ·
I maintainer di solito rispondono entro 2 giorni
Tutte le issue di rocq-prover/stdlib
Issue simili
-
@tailwindcss/vite: build transform returns map: undefined, causing SOURCEMAP_BROKEN under Vite 8/RolldownForse già presa @lazerg l’ha presa oggi. Aperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
tailwindlabs/tailwindcss#20622 ·
I maintainer di solito rispondono entro 1 giorno
-
area: server priority: P3 type: bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 83/100
appandflow/stim#4538 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
boykopovar/AnyPS5#12124 ·
I maintainer di solito rispondono entro 1 giorno
-
bug-unconfirmed
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
I maintainer di solito rispondono entro 1 giorno