repo, sorry, admit

Stream: condensed mathematics

[Johan Commelin]

I've made a couple of changes to the repo with the following effect:

If you now compile src/liquid.lean you should get only 2 warnings about sorry: one for thm95 and one for first_target.
The second sorry should be easy to fill in, by reducing it to thm95.

To make this possible, I have moved code that was sorryd to new files that are not in the dependency chain of src/liquid.lean. Of course they should end up in the dependency chain at some point, once they are sorry-free, and used in the proof of thm95.

I have also replace every occurence of sorry in commented code by the word admit, which is functionally equivalent (in tactic mode).
This means that we can now run

rg sorry | wc -l
12

to find that we have 12 lines containing uncommented sorrys (of which 2 are in the README).

[Patrick Massot]

Since you are in a cleaning up mood, could you get us rid of the undefined references in the blueprint? They are also generating a lot of noise.

[Johan Commelin]

I need to prepare a talk on type theory first...

[Johan Commelin]

But I think I'll stay in cleaning up mood for a couple of days, now that thm95 is in place.

[Johan Commelin]

We need to clean up the mess before we sprint onto the battlefield

[Johan Commelin]

 4 files changed, 787 deletions(-)
 delete mode 100644 src/Mbar/Mbar_pow.lean
 delete mode 100644 src/Mbar/breen_deligne.lean
 delete mode 100644 src/Mbar/complex.lean
 delete mode 100644 src/for_mathlib/continuous_map.lean

These files contain code that has been generalised in order to state thm 9.5. Repo just shrunk with about 10% (-;

[Johan Commelin]

Patrick Massot said:

Since you are in a cleaning up mood, could you get us rid of the undefined references in the blueprint? They are also generating a lot of noise.

I fixed those. But with a "hack". I just put things in a sort of appendix, and we should move them to a better place in the next refactor of the blueprint