[isabelle] Noteworthy Isabelle proof developments for a survey paper

[Talia Ringer]

Hi all,

My name is Talia Ringer and I'm a Ph.D. student at the University of
Washington. I'm working on a proof engineering
<http://proofengineering.org/> survey paper. However, I don't have any
Isabelle expertise on the paper, and my community overwhelmingly skews
toward Coq users. To make sure Isabelle gets adequate coverage, I have been
consulting other people.

Right now, I am looking for noteworthy Isabelle proof developments to
include in the paper. The paper focuses mostly on proof engineering for
program verification, but it talks about mathematics and metatheory as
well, so developments in those domains are welcome. I'm aware of the AFP,
but please don't hesitate to link to particular developments within the AFP
if you think they're especially noteworthy. It is OK to send your own work
if you think it is noteworthy and want to make sure it isn't missed.

Also, while not the focus of this email, feel free to send other bits of
Isabelle knowledge besides major proof developments that you think are
essential to a survey paper (to give an idea of what sorts of things are
relevant, we already talk about Isar, the Isabelle style guide, Nominal
Isabelle, Transfer and Lifting, sledgehammer, and Isabelle/jedit, among
other things).

Thank you,

Talia
http://tlringer.github.io/

[Buday Gergely]

Dear Talia,

https://ts.data61.csiro.au/projects/TS/proof-engineering/

is a good source for proof engineering using Isabelle.

- Gergely

-----Original Message-----
From: cl-isabelle-users-***@lists.cam.ac.uk <cl-isabelle-users-***@lists.cam.ac.uk> On Behalf Of Talia Ringer
Sent: Tuesday, August 7, 2018 1:47 AM
To: cl-isabelle-***@lists.cam.ac.uk
Subject: [isabelle] Noteworthy Isabelle proof developments for a survey paper

Hi all,

My name is Talia Ringer and I'm a Ph.D. student at the University of Washington. I'm working on a proof engineering <http://proofengineering.org/> survey paper. However, I don't have any Isabelle expertise on the paper, and my community overwhelmingly skews toward Coq users. To make sure Isabelle gets adequate coverage, I have been consulting other people.

Right now, I am looking for noteworthy Isabelle proof developments to include in the paper. The paper focuses mostly on proof engineering for program verification, but it talks about mathematics and metatheory as well, so developments in those domains are welcome. I'm aware of the AFP, but please don't hesitate to link to particular developments within the AFP if you think they're especially noteworthy. It is OK to send your own work if you think it is noteworthy and want to make sure it isn't missed.

Also, while not the focus of this email, feel free to send other bits of Isabelle knowledge besides major proof developments that you think are essential to a survey paper (to give an idea of what sorts of things are relevant, we already talk about Isar, the Isabelle style guide, Nominal Isabelle, Transfer and Lifting, sledgehammer, and Isabelle/jedit, among other things).

Thank you,

Talia
http://tlringer.github.io/

[Makarius]

Post by Talia Ringer
I'm working on a proof engineering
<http://proofengineering.org/> survey paper. However, I don't have any
Isabelle expertise on the paper, and my community overwhelmingly skews
toward Coq users. To make sure Isabelle gets adequate coverage, I have been
consulting other people.

The term "proof engineering" is rarely used in the Isabelle community,
although people are probably doing it implicitly all the time. From the
perspective of the prover platform, the strategy has always been to make
it perform sufficiently well, such that high-end applications are easily
processed by it without requiring further adhoc tools.

There has always been a race of system infrastructure vs. applications.
A current snapshot of it is sketched in my presentation at the Isabelle
Workshop 2018: "Further Scaling of Isabelle Technology" (slides and
paper) https://sketis.net/2018/slides-for-presentations-at-floc-2018-oxford

The slides classify time scales for processing Isabelle theory sessions
as follows:

* instantaneous: 10 min (Edmund Stoiber constant)
* online waiting: 45 min (Paris Commuter constant)
* offline waiting: 2 h (French Lunch time)
* too long: 8 h (Overnight job)


The best I have seen in recent months is as follows:

1) Intel Xeon 2 * 20 cores with SSD

* 2 min for the Isabelle/HOL image (the "standard prelude"), which is
already quite big
* 6 min for the main Isabelle/HOL libraries, including HOL and the
huge HOL-Analysis session
* 11 min for the full Isabelle distribution (libraries and examples)
* 36 min for Isabelle + AFP, excluding unusually slow sessions

2) AMD 8 * 8 cores cluster

* 65 min for Isabelle + AFP, including regular slow sessions,
excluding some special very-slow sessions (one of it takes 4-6h)

Post by Talia Ringer
I'm aware of the AFP,
but please don't hesitate to link to particular developments within the AFP
if you think they're especially noteworthy. It is OK to send your own work
if you think it is noteworthy and want to make sure it isn't missed.

I see AFP as the main application of Isabelle, and guess that it covers
approx. 60% of the visible Isabelle universe. Already since 2006,
Isabelle technology enhancements are driven by the requirements of AFP.

Post by Talia Ringer
to give an idea of what sorts of things are
relevant, we already talk about Isar, the Isabelle style guide, Nominal
Isabelle, Transfer and Lifting, sledgehammer, and Isabelle/jedit, among
other things.

Note on Isar: well-structured proofs are not only better for the human
reader (and maintainer), but also for overall system performance. People
sometimes think that "declarative proof languages" are expensive
concerning automated proof search, but Isar is not called "declarative"
and its built-in automation is minimal: Isar means "Intelligible
semi-automated reasoning". Consequently, checking well-structured Isar
proofs is much faster than old-style "apply" scripts (this a minority
style in Isabelle applications, but a majority style in Coq applications).

Note on Eisbach: this proof method language has been added in recent
years. Inspired by Ltac, it allows to define Isar proof methods in the
source notation of the proof language. Some Eisbach spin-off concepts
allow to structure old-style apply-scripts, e.g. the 'subgoal' command
(similar to Coq bullets, but leading to parallel proofs). Beyond that it
is easy to define proof methods in Isabelle/ML: unlike Coq with its
separate "plugin" concept, Isabelle tools are defined directly within
the theory source, and subject to the normal interaction model (and
Prover IDE support).

Note on Isabelle/jEdit (in that spelling): this is the main front-end of
Isabelle/PIDE --- the Prover IDE framework --- and the default
user-interface of Isabelle. Another PIDE front-end is Isabelle/VSCode,
which is included in Isabelle2018 at a relatively modest 1.1 version,
but some people have already started using it. Isabelle users
occasionally abuse the name of the "jEdit" text editor for the whole
technology stack behind the Isabelle/jEdit product. Conceptually, the
key things are Isabelle/Scala and Isabelle/PIDE: a hybrid of Scala and
ML modules to support IDE concepts natively in the prover.


In recent years there has been a tendency to integrate more and more
prover technology into the Prover IDE (according to its name and
principle). A notable exception is the "isabelle build" command-line
tool, but it will also move into the IDE eventually.

The build tool understands the syntax of Isabelle theory sessions. This
is important for scaling, and "engineering" of large proof projects: the
system can impose certain policies according to the theory structure.

Taking away the free choice of "make" tools from the user also means
that Isabelle projects can easily build on existing projects, without
having to worry about the underlying project management technology: it
is just standard Isabelle itself.


Makarius

[Makarius]

Post by Makarius
The slides classify time scales for processing Isabelle theory sessions
* instantaneous: 10 min (Edmund Stoiber constant)
* online waiting: 45 min (Paris Commuter constant)
* offline waiting: 2 h (French Lunch time)
* too long: 8 h (Overnight job)

Non-Bavarians often don't understand the Edmund Stoiber joke above. Here
is the original speech

as
representative of the many variations on the theme on Youtube. The
illustrations also help to get the point, despite Stoiber's strange way
of speaking German. (It is about building a high-speed train connection
from Munich main station to Munich airport, in order to get there in
max. 10 min. The project has not materialized so far.)


Related to that is the keynote by Peter O'Hearn at FLoC 2018 about
"Continuous Reasoning: Scaling the Impact of Formal Methods"
https://easychair.org/smart-program/FLoC2018/2018-07-09.html

He was talking about "diff time" of max. 15 min. It is the time you are
ready to invest to study the diff of an incoming changeset, to discuss
it with colleagues, decide to apply it or ignore it. His message to
formal-method tool builders: you need to be quicker than 15 min for
immediate formal analysis, if you want software developers to take your
results into account.

For formal proof checking the situation is analogous, but re-checking of
proofs is not optional, it cannot be ignored. Thus it is important to
have the main libraries and applications build in less than 10-15min in
order to remain productive in continued maintenance of the core system
and libraries.


Makarius

[Michal Wallace]

Post by Makarius
For formal proof checking the situation is analogous, but re-checking of
proofs is not optional, it cannot be ignored. Thus it is important to
have the main libraries and applications build in less than 10-15min in
order to remain productive in continued maintenance of the core system
and libraries.

Why isn't it optional?

Obviously, it can't be optional when building releases, but for day to day
work,
couldn't the library files be checked against a hash / signature, and the
corresponding internal proof objects be loaded "pre-proven" from a
binary file on startup when the signature hasn't changed?

(Part of my problem is that Isabelle crashes several times a day for me
on windows, and I have to restart jEdit. I've been told this is not usual,
but I don't yet know how to diagnose what's happening.)

[Michal Wallace]

Hrm. I see now that when I first install/load a new version, there is a
substantial "build time" where the libraries are processed.
Why does it still take a minute or so to verify the imported libraries when
opening a file for the first time in jEdit?

(Sorry, still making my way through the system/implementation manuals....)

Post by Makarius
For formal proof checking the situation is analogous, but re-checking of

Post by Makarius
proofs is not optional, it cannot be ignored. Thus it is important to
have the main libraries and applications build in less than 10-15min in
order to remain productive in continued maintenance of the core system
and libraries.

Why isn't it optional?
Obviously, it can't be optional when building releases, but for day to day
work,
couldn't the library files be checked against a hash / signature, and the
corresponding internal proof objects be loaded "pre-proven" from a
binary file on startup when the signature hasn't changed?
(Part of my problem is that Isabelle crashes several times a day for me
on windows, and I have to restart jEdit. I've been told this is not usual,
but I don't yet know how to diagnose what's happening.)

[Makarius]

Post by Michal Wallace
I see now that when I first install/load a new version, there is a
substantial "build time" where the libraries are processed.
Why does it still take a minute or so to verify the imported libraries when
opening a file for the first time in jEdit?

I am unsure which build time you mean exactly.

Isabelle2017 introduced an exploration of all potential theory imports
of all reachable sessions, with a penalty of 30s .. 90s (more on Windows).

This has become slightly faster in Isabelle2018-RC4, and there are
options to narrow the visible session space explicitly: see NEWS on
options -R -S -A -i for "isabelle jedit" (and "isabelle vscode").

You can also use these options to let the system build an auxiliary
session image, e.g. when there are many imports from other sessions that
you don't edit continuously.


Beyond that, much better Prover IDE support could mean:

* Session dependencies are explored on demand (this probably requires
to restrict theory sources strictly to the session directory).

* A dynamic session image for the interactive process is maintained
incrementally, like in the very old days of the Isabelle REPL and Emacs
mode, when it was all really slow (several minutes for a single one theory).


Makarius

[Makarius]

Post by Michal Wallace
Part of my problem is that Isabelle crashes several times a day for me
on windows, and I have to restart jEdit. I've been told this is not usual,
but I don't yet know how to diagnose what's happening.

The start is to report the problem publicly, and say which version of
Windows (and Isabelle) you are using. We are de-facto already on
Isabelle2018, see https://isabelle.in.tum.de/website-Isabelle2018-RC4

The release will become final soon, so it is the last chance to sort out
problems for the new Isabelle2018.

Post by Michal Wallace
Note on Isabelle/jEdit (in that spelling): this is the main front-end of
Isabelle/PIDE --- the Prover IDE framework --- and the default
user-interface of Isabelle. Another PIDE front-end is Isabelle/VSCode,
which is included in Isabelle2018 at a relatively modest 1.1 version,
but some people have already started using it. Isabelle users
occasionally abuse the name of the "jEdit" text editor for the whole
technology stack behind the Isabelle/jEdit product.

I have written earlier on this thread: """abuse the name of the "jEdit"
text editor for the whole technology stack behind the Isabelle/jEdit
product""" for a reasons, or actually two reasons:

(1) jEdit is a text editor project on its own that deserves more
acknowledgement and attention

(2) The Isabelle/jEdit/PIDE/Scala/ML technology stack can fail in
different spots. Step 0 of sorting this out is to develop a sense where
it fails and who is responsible for it. E.g. on Windows it could be the
Cygwin32 distribution in Isabelle2017, which is Cygwin64 in
Isabelle2018; or different Java versions managed by Oracle.


Makarius

[Makarius]

Post by Makarius

Post by Michal Wallace
Part of my problem is that Isabelle crashes several times a day for me
on windows, and I have to restart jEdit. I've been told this is not usual,
but I don't yet know how to diagnose what's happening.

The start is to report the problem publicly, and say which version of
Windows (and Isabelle) you are using. We are de-facto already on
Isabelle2018, see https://isabelle.in.tum.de/website-Isabelle2018-RC4
The release will become final soon, so it is the last chance to sort out
problems for the new Isabelle2018.

One more idea for remote diagnosis of problems: on Windows "anti-virus"
software occasionally causes delay the startup of external tools, e.g.
provers for Sledgehammer. This may cause odd crashes elsewhere.


Makarius

[Michal Wallace]

since installing rc4, I've yet to have a crash. (though I've also not had
as much time to play with Isabelle. :/)

Post by Michal Wallace

Post by Makarius

Post by Michal Wallace
Part of my problem is that Isabelle crashes several times a day for me
on windows, and I have to restart jEdit. I've been told this is not

usual,

Post by Makarius

Post by Michal Wallace
but I don't yet know how to diagnose what's happening.

The start is to report the problem publicly, and say which version of
Windows (and Isabelle) you are using. We are de-facto already on
Isabelle2018, see https://isabelle.in.tum.de/website-Isabelle2018-RC4
The release will become final soon, so it is the last chance to sort out
problems for the new Isabelle2018.

One more idea for remote diagnosis of problems: on Windows "anti-virus"
software occasionally causes delay the startup of external tools, e.g.
provers for Sledgehammer. This may cause odd crashes elsewhere.
Makarius