Testing infrastructure and bug fixes

[mpenciak]

This PR does a lot (sorry reviewers!):

• Removes the Arrays and TraitGenerics examples as these are just copies of the mtree_recover function from the Merkle and MerkleFromScratch examples
• Changes the CI as discussed to run only once on PRs
• Renames the CLI tool from cli to lampe
• Changes the initial Lake project generated by Lampe as follows:
  • Adds an import to the Extracted module in the main library file
  • Removes proven-zk as a default lake dependency
  • Removes the Extracted build target from the generated lakefile, as the current lampe
    generation places the extracted files as a submodule of the main library
  • Fixes the generated lean-toolchain file to the version used by Lampe
• Fixes the github runner running out of space by changing the testing script to build a lake-manifest.json file that points to an already-downloaded copy of mathlib.

In the course of fixing the above test infrastructure, a number of issues became apparent:

• The Lean syntax was elaborating a terminal let expression incorrectly. Before the body of:

nr_def foo<>() -> Unit {
    let a = 3 : Field;
}

would expand to Expr.letIn ... fun v => Expr.var v (incorrectly), and Lean would point out the type error. The new syntax expands this to Expr.letIn ... fun _ => Expr.skip.
Also fixes other terminal non-returning expressions from being interpreted as returns.

• Implements the std::mem::zeroed builtin
• Implements the Field != builtin
• Modifies the Experiments test/example to account for some open bugs on the Noir compiler (Catch unbound type variables earlier in compilation noir-lang/noir#7889) and (TBD)
• Re-adds infrastructure to test the extractor. This is mostly just helpful for debugging during development, and generally any test of this form should eventually be moved to the Examples folder eventually.