leanprover-community/ProofWidgets4

macOS build deadlocks nondeterministically

Ouverte

#33 ouverte le 8 nov. 2023

Voir sur GitHub
 (2 commentaires) (0 réaction) (0 personne assignée)Lean (45 forks)auto 404
bughelp wanted

Métriques du dépôt

Stars
 (219 étoiles)
Métriques de merge PR
 (Métriques PR en attente)

Description

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.

Guide contributeur

Direction de recherche
Reproduire le blocage localement sur macOS, surveiller les processus npm parasites et vérifier si le problème vient de npm ou de Rollup.js en exécutant manuellement les étapes de construction.
Stack technique
javascript
Domaine
build system
Type d'issue
Bug
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-2 jours
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Investigation requise
Prérequis
LeanmacOSnpm
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
40