search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
134 stars 33 forks source link

[RFC] Removing the Why3 parser #642

Open Halbaroth opened 1 year ago

Halbaroth commented 1 year ago

Alt-Ergo supports a subset of the why3 format as input through the plugin AB-why3, see https://ocamlpro.github.io/alt-ergo/Plugins/index.html#ab-why3-plugins.

This feature can be activated by using the option --add-solver in order to add the custom parser. I think this is the only use of the option add-solver.

Besides, the plugin uses the AST parsed.mlof the legacy parser, which means we have to rewrite it before removing the legacy parser in order to produce the Dolmen AST.

Should we keep this feature?

Halbaroth commented 11 months ago

We'll remove this feature when we get rid of the legacy parser. As the legacy parser is deprecated in v2.6.0 and this feature works only with the legacy parser, we don't need to deprecate too.