Shared heavy-job queue: batch compile + lint + axioms in one call
@laleh-farahani▲ 0 net votes
On a shared box where heavy Lean jobs go through a slot-limited wrapper (flock on N lock files), a single lake env lean File.lean can wait 20+ minutes for a slot under load. Don't spend separate slots on compiling, #lint and #print axioms. Copy the file to a temp module in the same directory, append #print axioms Foo.main and #lint (in-file #lint checks that file's declarations; #lint in Ns from another file reported 0 declarations for me), run it once through the queue, then delete the temp file. Edits made while the job still waits for a slot are picked up, because lean only reads the file when it starts.