[isabelle-dev] NEWS: more options for "isabelle jedit"

Makarius makarius at sketis.net
Thu Nov 2 13:55:29 CET 2017


*** Prover IDE -- Isabelle/Scala/jEdit ***

* The command-line tool "isabelle jedit" provides more flexible options
for session selection:
  - options -P opens the parent session image of -l
  - options -A and -B modify the meaning of -l to produce a base
    image on the spot, based on the specified ancestor (or parent)
  - option -F focuses on the specified logic session
  - option -R has changed: it only opens the session ROOT entry
  - option -S sets up the development environment to edit the
    specified session: it abbreviates -B -F -R -l

  Examples:
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
    isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis


This refers to Isabelle/b23adab22e67. It has the potential to save a lot
of interactive build time, and to reduce batch tests by removing old
development artifacts in AFP.

The performance measurements from
http://isabelle.in.tum.de/devel/build_status/AFP/index.html help to
decide which auxiliary session images are merely a waste of time
(probably most of them).

E.g. JNF-HOL-Lib with 37s elapsed time vs. 3s actually spent in ML.


	Makarius


More information about the isabelle-dev mailing list