Some sorry's in Lean files

Stream: Equational

[Bruno Le Floch]

The Lean code includes some sorry and TODO, should we address them before making a snapshot of the code for arXiv/journal submission?

List of files with sorry

blueprint/web/js/graphvizlib.wasm
equational_theories/Generated/EquationSearch/README.md
equational_theories/Generated/EquationSearch/src/dont_be_sorry.rb
equational_theories/Generated/EquationSearch/src/search.rb
equational_theories/Generated/Greedy/src/forcer_leanify.py
equational_theories/Definability/Law43.lean
equational_theories/Definability/Law46.lean
equational_theories/ForMathlib/Definability.lean
equational_theories/FactsSyntax.lean
home_page/implications/to_lean.js

Most of them are perfectly fine, but the Definability ones look like unfinished code, e.g., equational_theories/Definability/Law43.lean. This is clearly not part of the formalization of the implication graph, but it is worrisome that there could be some sorry anywhere in the repository.

Maybe we should also clean up any TODO?

Files including TODO

docs/graph_operations.md
equational_theories/Generated/VampireProven/src/vampire_proofs_cyc.py
equational_theories/Generated/FiniteImplicationSearch/src/generate_tptp.rb
equational_theories/Generated/EquationSearch/src/search.rb
equational_theories/Generated/Greedy/src/forcer.py
equational_theories/Generated/FinSearch/src/finsearch.py
equational_theories/Generated/Confluence/src/find_confluent_equations.py
equational_theories/ParseImplications.lean
equational_theories/FreshGenerator.lean
equational_theories/Definability/Law43.lean
equational_theories/ForMathlib/Definability.lean
equational_theories/ManuallyProved/Equation713.lean
equational_theories/ManuallyProved/Equation1447.lean
equational_theories/ManuallyProved/Equation1701.lean
equational_theories/LiftingMagmaFamiliesCounterexamples.lean
equational_theories/LinearOps.lean
equational_theories/Z3Counterexamples.lean
equational_theories/Superposition.lean
equational_theories/LiftingMagmaFamilies.lean
equational_theories/Obelix.lean
equational_theories/FullSpectrum.lean
home_page/index.md
home_page/fme/elm.js
paper/main.log
paper/statistics.tex
paper/automated.tex
paper/main.tex
README.md
scripts/graph.rb
tools/fme/dist/elm.js
widget/rollup.config.js
widget/dist/HasseDiagram.js

[Cody Roux]

Probably worth nothing that probably all non trivial software contains TODOs, and many mature formalizations contain sorrys (or their equivalent)

[Bruno Le Floch]

TODOs I can understand (and I've left my share of them in the LaTeX kernel), but I'm surprised about sorry. How can a reviewer check that we tracked properly the lack of sorry in the statements that we claim to be formalized?

[Kevin Buzzard]

#print axioms name_of_statement

[Aaron Hill]

We also have some custom metaprogramming code that essentially checks the output of #print axioms on each implication/non-implication theorem

[Aaron Hill]

https://github.com/teorth/equational_theories/blob/e3f3425189f41a663a6a4ad5702a9a25ed86c0cd/equational_theories/EquationalResult.lean#L95

[Alex Meiburg]

I think I'm responsible for checking those two sorries in to the repo. Of those files you listed, only four are .lean, and two of those (FactsSyntax.lean and Definability.lean) only have sorry in comments. Which leaves just the Law43.lean and Law46.lean. Each of which has one sorried theorem.

These were from me exploring relatively definable equations, which ... some day, would be nice to revisit and do more study of. But it never became a "real" part of the final product here.