Re: [isabelle-dev] NEWS: more options for "isabelle jedit"
On 04/11/17 10:25, Florian Haftmann wrote: > > Lets start with > > isabelle jedit -d '$AFP' -S … > > This provides a suitable base image and opens the ROOT file. > > What is the canonical way to proceed from there to check the whole > session? Of course the ROOT file lists the respective theories and you > can open them manually in jedit, but this is tiresome if the ROOT file > spans many theories. > > Would clicakble theorie files in ROOT files be an option? Clickable ROOT now works in Isabelle/62a5fbdded50. Beyond that, I would like to see eventually a Theories or Session dockable with systematic access to all theories from certain sessions. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: more options for "isabelle jedit"
Dear Makarius, > *** 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 is really great and makes my life significantly easier! There remains one gap which I am wondering how to fill it. Lets start with isabelle jedit -d '$AFP' -S … This provides a suitable base image and opens the ROOT file. What is the canonical way to proceed from there to check the whole session? Of course the ROOT file lists the respective theories and you can open them manually in jedit, but this is tiresome if the ROOT file spans many theories. Would clicakble theorie files in ROOT files be an option? Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: more options for "isabelle jedit"
*** 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
