Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to edit the Isabelle sources?


view this post on Zulip Email Gateway (Aug 05 2020 at 13:48):

From: Mario Carneiro <di.gama@gmail.com>
I would like to hack on the isabelle kernel, but I don't have a very good
understanding of the bootstrapped architecture. Is there a documentation
source that describes how I can make a change to the source (in jedit,
say), rebuild it, and see the effect in my Scratch.thy? I don't mind
breaking my distribution. I'm working from the Isabelle2020 distribution on
Ubuntu.

I recall there is something to do with passing command line arguments to
isabelle, but I don't know any details; I think you have to pass the name
of a theory? (I'm only interested in Isabelle/Pure for the present, with
little to no theory imported, to keep things simple.)

Mario Carneiro

view this post on Zulip Email Gateway (Aug 05 2020 at 14:40):

From: Makarius <makarius@sketis.net>
On 05/08/2020 15:47, Mario Carneiro wrote:

I would like to hack on the isabelle kernel, but I don't have a very good
understanding of the bootstrapped architecture. Is there a documentation
source that describes how I can make a change to the source (in jedit,
say), rebuild it, and see the effect in my Scratch.thy? I don't mind
breaking my distribution. I'm working from the Isabelle2020 distribution on
Ubuntu.

Here are some relevant command-line invocations:

cd Isabelle2020

# edit Isabelle/Pure sources
isabelle jedit -l Pure src/Pure/ROOT.ML &

# test that it really works
isabelle build Pure

# restart above Isabelle/jEdit with new Pure image

The documentation for command-line options of "isabelle jedit" is in the
Documentation panel entry "jedit", and for "isabelle build" entry "system".

I recall there is something to do with passing command line arguments to
isabelle, but I don't know any details; I think you have to pass the name
of a theory? (I'm only interested in Isabelle/Pure for the present, with
little to no theory imported, to keep things simple.)

As sketched above you can edit Pure itself: it requires somewhat special tricks.

If you want to edit anything on top of Pure, you merely start "isabelle jedit
-l Pure" and then open the other theories you are interested in (e.g.
src/HOL/Main.thy). You can't edit/change the running Pure without restarting
the Prover IDE.

Makarius


Last updated: Sep 28 2021 at 20:18 UTC