We currently use myth to synthesize terms, but myth only supports a subset of the ocaml. This leads to a number of translation issues. We need to replace this with the new gallina synthesizer (being developed in https://github.com/qsctr/coq-synth).
We need to integrate coq-synth to lfind as an external binary call. If we try to call coq-synth as a library we face dependency issues with lfind plugin environment.
qsctr
commented
2 years ago
We currently use myth to synthesize terms, but myth only supports a subset of the ocaml. This leads to a number of translation issues. We need to replace this with the new gallina synthesizer (being developed in https://github.com/qsctr/coq-synth).
We need to integrate coq-synth to
lfindas an external binary call. If we try to call coq-synth as a library we face dependency issues withlfindplugin environment.Similar to how we provide definitions and examples to
lfind, we need to provide examples to coq-synth (see https://github.com/qsctr/coq-synth/issues/1).