dump.ml does not compile anymore

[gares]

since it was written 10 years ago ;-)

[spitters]

What would go into getting it to work again? @VincentSe has a cool application in mind.

[VincentSe]

@gares @spitters According to the documentation
https://coq.github.io/doc/master/refman/practical-tools/utilities.html
The VERNAC EXTEND must be in a mlg file for preprocessing, so dump.ml cannot work anymore.

[spitters]

This should now be rewritten as a plugin, which I hope would not be too difficult.

[gares]

This is a small totorial for writing plugins: https://github.com/coq/coq/tree/master/doc/plugin_tutorial

[VincentSe]

@spitters @gares Indeed, we can run the ocaml compiler by putting dump.ml inside g_tuto0.mlg. And we then see multiple errors

• modules Topconstr, Pretyping.Default and Tactic no longer exist
• pp function names changed, I am not sure which ones to call now
• Reductionops changed, I tried rewriting it by this (Reductionops.nf_all env Evd.empty c) but it fails with This expression has type (EConstr.constr -> Tacticals.tactic) -> Tacticals.tactic but an expression was expected of type EConstr.constr = Evd.econstr. I have no clue what that means.

[gares]

If you publish your wip branch I can look at it.

[VincentSe]

@gares Here is the branch
https://github.com/coq-community/corn/tree/FixDump
At the moment it is just a copy of tuto0 into dump. The code in dump.ml was moved into g_tuto0.mlg, type make in folder dump to build and see the errors. I'll rename tuto0 when it compiles and works.

[VincentSe]

Hello @gares, did you look at the branch I sent you ?

[gares]

Sorry I was on VAC. I see you merged the branch, cool!