search

OCamlPro / alt-ergo

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

[RFC] Remove dynlinked parsers #266

Closed Gbury closed 2 weeks ago

Gbury commented 4 years ago

Following the recent addition of Gbury/dolmen (that will allow alt-ergo to more input languages such as smtlib, tptp, etc...), we are considering potentially removing the support for dynlinked parsers, as this would allow to remove the entire legacy parsers and typechecker.

Before the removal, support for the native alt-ergo language as well as why3 will be added to dolmen so that no current capabilities of alt-ergo will be lost. However dolmen does not currently support dynlinking additional parsers, so we'd like to evaluate how much that feature is used, so please comment here if you are using dynlinked parsers or are planning on using them, ^^

Halbaroth commented 2 weeks ago

The support of custom parsers have been removed in #1251 and the deprecated AB-Why3 plugin was the only part of the code which used the Why3 parser. This plugin have been deprecated in v2.6.0 and removed in #1251 too.