[isabelle] Isabelle2014 and ProofGeneral



Can Isabelle2014 work with ProofGeneral at all?  The NEWS file says:

 Proof General with its traditional helper scripts is now an optional
 Isabelle component, e.g. see ProofGeneral-4.2-2 from the Isabelle
 component repository http://isabelle.in.tum.de/components/.  Note that
 the "system" manual provides general explanations about add-on
 components, especially those that are not bundled with the release.

So I unpacked the PG tarball.  Within it is the directory isar and files
isar/interface and isar/README.  And the latter says:

 The script `interface' and file 'interface-setup.el' are used
 internally to start Isabelle Proof General via the 'isabelle' shell
 command.  This is the default way to invoke Proof General from the
 Isabelle perspective; it enables Isabelle to provide a consistent
 process and file-system environment, including the all-important
 isar-keywords.el file.

But:

$ /opt/Isabelle2014/bin/isabelle
### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)
### Using bulky 64bit version of Poly/ML instead

Usage: isabelle NAME [ARGS ...]

  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.

Available tools:
  browser - Isabelle graph browser
  build - build and manage Isabelle sessions
  codegen - issue code generation from shell
  components - resolve Isabelle components
  console - run Isabelle process with raw ML console and line editor
  display - display document (in DVI or PDF format)
  doc - view Isabelle documentation
  document - prepare theory session document
  env - run a program in a modified environment
  getenv - get values from Isabelle settings environment
  haskabelle - Haskabelle interface wrapper
  install - install standalone Isabelle executables
  java - invoke Java within the Isabelle environment
  jedit - Isabelle/jEdit interface wrapper
  keywords - generate keyword files for Emacs Proof General
  latex - run LaTeX (and related tools)
  logo - create an instance of the Isabelle logo
  mirabelle - testing tool for automated proof tools
  mkroot - prepare session root directory
  mutabelle - mutant-testing for counterexample generators and automated tools
  options - print Isabelle system options
  scala - invoke Scala within the Isabelle environment
  scalac - invoke Scala compiler within the Isabelle environment
  tptp_graph - TPTP visualisation utility
  tptp_isabelle - Isabelle tactics for TPTP competitive division
  tptp_isabelle_hot - Isabelle tactics for TPTP demo division
  tptp_nitpick - Nitpick for TPTP
  tptp_refute - Refute for TPTP
  tptp_sledgehammer - Sledgehammer for TPTP
  tptp_translate - translate between TPTP formats
  update_sub_sup - update Isabelle symbols involving sub/superscripts
  version - display Isabelle version
  yxml - simple XML to YXML converter


... no obvious way to start PG.


So, is this a miscommunication between the 2 projects, missing
documentation, or has PG interface simply been dropped altogether?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.