Il worker di lungo esegue durante la build codice Lean del tuo progetto e delle sue dipendenze. Questa guida mostra come limitarne il tempo e la memoria e come isolarlo dal tuo ambiente, per esempio in CI.
Limita il tempo
Per fermare una build che dura troppo, imposta un limite di tempo reale:
use std::time::Duration;
fn main() -> lungo_build::Result<()> {
lungo_build::configure().worker_timeout(Duration::from_secs(600)).compile_lean("lean")
}
Quando il limite scade, il worker e ogni processo che ha avviato vengono terminati e la build
fallisce con LNG0304.
Per limitare invece il tempo di processore (un ciclo che non termina, più che una macchina
lenta), usa .worker_cpu_limit(Duration::from_secs(300)); superarlo fa fallire la build con
LNG0305. Su Unix il limite si applica a ciascun processo
del worker; su Windows a tutti insieme.
Limita la memoria
.worker_memory_limit(8 << 30) // 8 GiB
Il limite è applicato su Linux (spazio di indirizzamento di ciascun processo del worker) e su
Windows (memoria dei processi del worker nel loro insieme). Lean mappa in memoria i file
compilati di ogni modulo importato, quindi lascia margine oltre a ciò che serve a
lake build. Su altri sistemi, come macOS, impostarlo fallisce con
LNG0104 invece di essere ignorato; impostalo solo per le
piattaforme che lo applicano:
let mut config = lungo_build::configure();
if cfg!(any(target_os = "linux", windows)) {
config = config.worker_memory_limit(8 << 30);
}
config.compile_lean("lean")
(In uno script di build cfg! descrive l’host, cioè dove gira il worker.)
Isola l’ambiente
.hermetic(true) esegue il worker con un ambiente minimo (percorsi, home, directory
temporanee, locale, elan) invece del tuo, così variabili come LEAN_PATH o credenziali non
raggiungono mai il codice Lean. .hermetic_worker_cache(true) compila il worker dentro
l’output della build invece che nella cache condivisa nella tua directory home.
Questi limiti contengono le build fuori controllo. Non isolano l’accesso al file system o alla rete; vedi Fiducia e verifica.