leanprover-community/ProofWidgets4

macOS build deadlocks nondeterministically

Aperta

#33 aperta il 8 nov 2023

Vedi su GitHub
 (2 commenti) (0 reazioni) (0 assegnatari)Lean (45 fork)auto 404
bughelp wanted

Metriche repository

Star
 (219 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

As seen here for example. My conjecture there was that this is due to the mutex in the lakefile.lean, but reproducing it locally it seems that there is sometimes a stray npm run build -- --tsxName <blah> process that never exits. This would suggest that the issue is actually something with NPM or Rollup.js.

Guida contributor

Direzione di ricerca
Riprodurre il deadlock localmente su macOS, monitorare i processi npm fuoriusciti e verificare se il problema è con npm o Rollup.js eseguendo manualmente i passaggi di build.
Tech stack
javascript
Dominio
build system
Tipo issue
Bug
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Richiede indagine
Prerequisiti
LeanmacOSnpm
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
40