Page MenuHomeIsabelle/Phabricator

Component and Isabelle/ML setup for Zipperposition
Open, NormalPublic


Provide proper setup for Zipperposition, with the usual production quality standards.

Related Objects

Event Timeline

makarius triaged this task as Normal priority.Thu, Oct 29, 4:21 PM
makarius created this task.

Isabelle/aca85e8d873d already provides isabelle build_zipperposition from the OPAM entry version 1.6, but this is rather old.

Proper inclusion in Isabelle might require:

  • to update the OPAM version
  • or to change the isabelle build_zipperposition tool to build from the repository (this might be more work, due to OCaml dependency hell on multiple platforms)