4.2.1 Do I lose my proofs when I clean a project?

No! This is a common misunderstanding of what a project clean does. A project contains two kinds of files:

• those you can edit: contexts, machines, proofs

• those generated by a project build: proof obligations, proof statuses (each proof obligation is either discharged or not discharged)

The cleaner just undoes what the builder does, i.e. it removes proof obligations and statuses, but it never modifies any proof.

A status may change from discharged to not discharged when the proof is no longer compatible with the corresponding proof obligation (e.g. when a hypothesis is changed), but the proof itself is still there! You can try to replay it.

Confusion may arise when automatic provers have been launched. The cleaner does not undo these automatic proofs (why would it ?!!). Once a proof has been made, the platform does not modify or delete it by itself. Even obsolete proofs are preserved (3.4.7.1)!