Documentazione di lungo

Come diagnosticare una build di lungo che fallisce

Risali da una cargo build che fallisce alla sua causa, tramite il codice di errore.

In questa sezione

Questa guida mostra come risalire da una cargo build che fallisce alla sua causa. Ogni errore di lungo inizia con un codice, error[LNGxxxx]; il riferimento degli errori li descrive uno per uno.

Trova il messaggio

Cargo stampa l’errore dello script di build sotto --- stderr:

error: failed to run custom build command for `shapes v0.1.0`
  ...
  --- stderr
  Error: error[LNG0201]: Lean elaboration failed

Leggi il codice, poi segui la sezione del suo intervallo.

Errori di Lean (LNG0201)

Il messaggio contiene la diagnostica di Lean con file, riga e colonna. Correggi il codice Lean; per iterare più in fretta, compila direttamente il progetto Lean:

cd lean && lake build

Errori di progetto e toolchain (LNG01xx)

  • La toolchain non è installata (LNG0103): esegui il comando indicato dal messaggio, elan toolchain install <toolchain>.
  • La toolchain non è supportata (LNG0102): fissa una toolchain supportata in lean-toolchain (vedi piattaforme).
  • Il manifest manca oppure una dipendenza non è materializzata (LNG0101): esegui una volta lake update nel progetto Lean e fai il commit di lake-manifest.json. Per un manifest esistente, lungo setup materializza le sue dipendenze senza modificarlo.
  • La configurazione non può avere effetto (LNG0107): il messaggio indica l’impostazione. Un percorso di modellazione che non seleziona nulla di solito è scritto male; lungo mappings elenca i nomi Lean di ogni tipo, funzione e campo generato.

Errori degli extern (LNG04xx)

Per LNG0401, il messaggio indica la dichiarazione, il simbolo, il tipo Lean e la posizione nel sorgente. Se la dichiarazione è tua, implementala e mappala (Come chiamare funzioni Rust da Lean). Se appartiene a una dipendenza, la dipendenza si basa su codice nativo che lungo non fornisce; implementa il simbolo in Rust con rust_extern, oppure evita la dichiarazione.

lungo externs elenca come è implementato ogni extern del programma.

Errori del worker (LNG03xx)

  • Timeout e limiti di risorse (LNG0304, LNG0305): alza il limite, oppure trova il codice Lean che impiega molto tempo durante l’elaborazione (lo mostra anche lake build).
  • Crash (LNG0303): il messaggio contiene l’output del worker. Esegui lungo prepare, che verifica il worker in cache e lo ricompila se è danneggiato; se il crash persiste, segnalalo con quell’output.
  • Richieste non soddisfacibili (LNG0301): confronta i nomi in root_module, export ed export_module con il progetto Lean. Un pacchetto senza defaultTargets richiede root_module.

Errori che indicano un difetto di lungo

LNG0302, LNG0404 e LNG05xx significano che lungo non è riuscito a gestire un output del compilatore valido. Segnalali con il messaggio, la toolchain Lean e, se possibile, lungo ir <declaration> per la dichiarazione indicata.