Page MenuHomeIsabelle/Phabricator

Component and Isabelle/ML setup for Zipperposition
Closed, ResolvedPublic

Description

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

Event Timeline

makarius triaged this task as Normal priority.Oct 29 2020, 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)

Isabelle/4a652d3f4522 provides isabelle build_zipperposition for 2.0 from OPAM. It works uniformly for Linux, macOS, Windows/Cygwin.

makarius claimed this task.

See Isabelle/162b71f7e554 and Isabelle/11de287ed481.