Re: [isabelle-dev] Isabelle release
On 07/01/11 20:07, Michael Norrish wrote: On 7/01/11 8:05 PM, Alexander Krauss wrote: But then we need a Marketing division to come up with a new name every 8 months :-}. Year numbers are very comfortable. You either come up with a set of names to use, or just do what most software projects do (commercial and open source both), and use numbers. Does the gcc project have this problem? Does Linux? Does emacs? Decide retroactively that everything up until this point was Isabelle 1, and announce the release of Isabelle 2. Or whatever set of numbers floats your boat... Taking a page from a successful marketing campaign, we could also adopt a variation on the Ubuntu way of naming things, two numbers: year and month. So this would be Isabelle 10.01. We can even add silly names like Anomalous Assumption, Bound Beta, Circular Coinduction, Dramatic Datatype, Epic Elimination, etc. I thought this might be a bit too silly to send to the dev list, but a third party encouraged me to do so anyway :) Rafal Kolanski. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Modest proposal for image tagging
Dear Isabelle Developers,
The problem:
There exist situations whereupon we find ourselves with an Isabelle
image file without knowing what exactly it is.
One such situation is using wwwfind to present multiple images on
multiple ports. One cannot expect users to remember which is which just
based on the port number. It is much more useful to have the image name
in the title.
Combined with a regression test system which automatically refreshes
such images, it is also pertinent to know which repository revision the
particular image was built from. This is also true when copying images
between machines that would normally take hours to build (e.g. grabbing
them from the regression test server in the morning).
Isabelle (well, the normal release one) currently does not have such a
feature.
An approach:
Now, Makarius will doubtless tell me I've done it wrong, but within our
project I have added a global val image_identifier string in every
image which at least has the name of the image, along with any other
identifying features. Then I added the -I option to isabelle usedir
which allows one to specify those identifying features. I then modified
wwwfind to display this string in the title.
So for example, when we build one of our images, we use:
IMAGE_IDENTIFIER_TAG = `hg log -l 1 --template '{node} {date|isodate}\n'
-r .`
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -I
$(IMAGE_IDENTIFIER_TAG)
Then if we connect to our wwwfind server on a given port, the title reads:
Find Theorems: CREFINE (7a95fca6ca33e071fd1c948a559898af7e21697e
2011-06-24 20:11 +1000)
If we pull the image off the server, we can also get this string by
evaluating image_identifier.
I think that this style of feature would be really nice in Isabelle. I
am also attaching a patch for Isabelle 2009-1 for your consideration.
If there is interest, I can port it to 2011, but I'd like to get some
feedback first.
Sincerely,
Rafal Kolanski.
summary: Added image_identifier functionality to isabelle images.
diff --git a/lib/Tools/usedir b/lib/Tools/usedir
--- a/lib/Tools/usedir
+++ b/lib/Tools/usedir
@@ -33,6 +33,7 @@
echo -s NAME override session NAME
echo -t BOOL internal session timing (default false)
echo -v BOOL be verbose (default false)
+ echo -I STRINGadd STRING to image_identifier val in image (default \\)
echo
echo Build object-logic or run examples. Also creates browsing
echo information (HTML etc.) according to settings.
@@ -87,11 +88,12 @@
PARALLEL_PROOFS=1
TIMING=false
VERBOSE=false
+IMAGE_IDENTIFIER_TAG=
function getoptions()
{
OPTIND=1
- while getopts C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v: OPT
+ while getopts C:D:M:P:T:V:bd:f:g:i:m:p:q:rs:t:v:I: OPT
do
case $OPT in
C)
@@ -169,6 +171,9 @@
check_bool $OPTARG
VERBOSE=$OPTARG
;;
+ I)
+IMAGE_IDENTIFIER_TAG= ($OPTARG)
+;;
\?)
usage
;;
@@ -236,7 +241,7 @@
LOG=$LOGDIR/$ITEM
$ISABELLE_PROCESS \
--e Session.use_dir \$ITEM\ \$ROOT_FILE\ true [$MODES] $RESET $INFO \$DOC\ $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \$PARENT\ \$SESSION\ ($COPY_DUMP, \$DUMP\) \$RPATH\ $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; \
+-e val image_identifier = \${NAME}${IMAGE_IDENTIFIER_TAG}\; Session.use_dir \$ITEM\ \$ROOT_FILE\ true [$MODES] $RESET $INFO \$DOC\ $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \$PARENT\ \$SESSION\ ($COPY_DUMP, \$DUMP\) \$RPATH\ $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS; \
-q -w $LOGIC $NAME $LOG
RC=$?
else
diff --git a/src/Pure/mk b/src/Pure/mk
--- a/src/Pure/mk
+++ b/src/Pure/mk
@@ -93,6 +93,7 @@
-e use\$COMPAT\ handle _ = exit 1; \
-e structure Isar = struct fun main () = () end; \
-e ml_prompts \ML \ \ML# \; \
+-e val image_identifier = \RAW\; \
-q -w RAW_ML_SYSTEM RAW $LOG 21
RC=$?
elif [ -n $RAW_SESSION ]; then
@@ -114,6 +115,7 @@
-e val ml_platform = \$ML_PLATFORM\; \
-e (use\$COMPAT\; use\ROOT.ML\) handle _ = exit 1; \
-e ml_prompts \ML \ \ML# \; \
+-e val image_identifier = \Pure\; \
-f -q -w RAW_ML_SYSTEM Pure $LOG 21
RC=$?
fi
diff --git a/src/Tools/WWW_Find/find_theorems.ML b/src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML
+++ b/src/Tools/WWW_Find/find_theorems.ML
@@ -66,7 +66,9 @@
fun html_header thy_name args =
html { lang = en } [
-head { title = Find Theorems: results, stylesheet_href = /basic.css }
+(* use global image_identifier which should be defined in all images *)
+head { title = Find Theorems: ^ image_identifier,
+ stylesheet_href = /basic.css }
[script (noid, { script_type=text/javascript,
src=/find_theorems.js })],
add_script (OnLoad, encodequery(document.getElementById('query')))
___
isabelle-dev
[isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
When I wanted to customize my symbol font when switching to JEdit, I
realized that:
1. There is no separate symbol font setting, but JEdit does supply a
nice cascading font substitution system (if glyph not found in
main font, try next, then next, until optionally try every one
in the system). It even lets you specify font sizes so their
metrics match!
2. The Isabelle plugin doesn't use it. We do get a etc/symbols file,
but it's a bit of an oddity. Unlike other parts of Isabelle source
code which use parser combinators, this is thrown together with
regular expressions.
The lookup system then depends on compressing a maximum of two
fonts plus other meta information (subscript, superscript, bold)
for every JEdit chunk type (19 types) into a single Java byte...
which is signed, so 127 tags is maximum. Is this done for speed?
It's a bit of a shock to new users that after they specify their
fonts the way they like, when JEdit loads everything looks great
for a few seconds, and then most symbols turns to rectangles when
the Isabelle plugin loads.
I'd be willing to try address this issue, but I don't know if
Makarius already has this in his pipeline already. I know it's
pointless to try submit patches when work is already planned
in accordance with a larger vision.
3. Trying to specify a font with a space in the name (e.g. Arial
Unicode MS, Cambria Math) doesn't work, because the config lines
in etc/symbols are split on \s+
Look, I realize I'm probably one of a handful of people on the planet
who specifies their own font preferences and color schemes, but I'd
appreciate the ability to do so. Call it being aesthetically challenged.
Attached is a workaround for Isabelle-2015, modifying
src/Pure/General/symbol.scala to allow escaping spaces when splitting
fields in etc/symbols.
I'm also sitting on two patches:
- Work around the mouse select copy-paste issue for output/query/etc
buffers.
This is because the JEdit '%' register is updated for TextArea
(see org/gjt/sp/jedit/textarea/MouseHandler.java ) when mouse is
dragged, but for the Isabelle Pretty_Text_Area it isn't.
Something a bit odd is going on here, because Rich_Text_Area inherits
the correct behaviour implicitly, but not when it's included
in Pretty_Text_Area. Maybe this needs more thinking.
- Removes hardcoded colors in favor of looking up relevant JEdit
properties. This is critical if you want a light-on-dark setup.
Also in patches/extended_styles style[0] is hardcoded to black
in org/gjt/sp/util/SyntaxUtilities.java. This should really look
up the view.fgColor property in JEdit!
Generally, defaulting to BLACK for foreground is inflexible, use:
jEdit.getColorProperty(view.fgColor)
same for 255,255,255 for a background, try use:
jEdit.getColorProperty(view.bgColor)
Any interest in these? Does anyone else care?
Sincerely,
Rafal Kolanski
diff --git a/src/Pure/General/symbol.scala b/src/Pure/General/symbol.scala
index b22613b..0d1e672 100644
--- a/src/Pure/General/symbol.scala
+++ b/src/Pure/General/symbol.scala
@@ -276,24 +276,24 @@ object Symbol
private class Interpretation(symbols_spec: String)
{
/* read symbols */
-
private val No_Decl = new Regex((?xs) ^\s* (?: \#.* )? $ )
private val Key = new Regex((?xs) (.+): )
private def read_decl(decl: String): (Symbol, Properties.T) =
{
def err() = error(Bad symbol declaration: + decl)
+ def unescape_space(s : String) : String = s.replace(\\ , )
def read_props(props: List[String]): Properties.T =
{
props match {
case Nil = Nil
case _ :: Nil = err()
- case Key(x) :: y :: rest = (x - y) :: read_props(rest)
+ case Key(x) :: y :: rest = (x - unescape_space(y)) :: read_props(rest)
case _ = err()
}
}
- decl.split(\\s+).toList match {
+ decl.split((?=[^])\\s+).toList match {
case sym :: props if sym.length 1 !is_malformed(sym) =
(sym, read_props(props))
case _ = err()
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
On 12/11/15 16:45, Japheth Lim wrote: > [...] > A lot of space could be saved if Isabelle saves heaps in this way. For > our L4.verified project we found a 7× reduction in size. I would like to add that the 7x reduction is from 50GB for a full build of all our heaps (i.e. regression test). This allowed me to keep using my 250GB SSD, whereas previously I was struggling with space issues for weeks. When Japheth committed this little change, my jaw just about hit the floor. No adverse effects so far. Thumbs up. Rafal Kolanski. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
On 15/11/15 02:24, Makarius wrote: > On Fri, 13 Nov 2015, Rafal Kolanski wrote: > >> On 12/11/15 16:45, Japheth Lim wrote: >>> [...] >>> A lot of space could be saved if Isabelle saves heaps in this way. For >>> our L4.verified project we found a 7× reduction in size. >> >> I would like to add that the 7x reduction is from 50GB for a full build >> of all our heaps (i.e. regression test). This allowed me to keep using >> my 250GB SSD, whereas previously I was struggling with space issues for >> weeks. When Japheth committed this little change, my jaw just about hit >> the floor. >> >> No adverse effects so far. Thumbs up. > > I usually trust David Matthews doing great things. > > Just formally, any change to make it into the official producation > quality version of Isabelle needs some extra efforts. It happens > routinely that old questions in the vicinity of a new feature need to be > revisited. If this is not done, there is a slow degration of overall > structural integrity of the system. > > One needs to resist from an attitude like "works for me, all great, no > problems, just do it". I never said "just do it". I said "thumbs up. That means the change caused very significant positive effects and I second the desire to have it looked at seriously in order to discover and mitigate any negative effects. I just have none to report. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On 16/11/15 07:14, Makarius wrote: > I have lost track of the status of this thread, with its various > side-threads on isabelle-users, isabelle-dev, and private mail. All the patches I have sent out are still in effect w.r.t font rendering. > In the meantime the situation is as follows: > > * jEdit-5.3.0 has been released a few weeks ago, and we are using it since > Isabelle/d40f906bb13f. > > * I am still waiting for various plugin updates, notably Navigator. > > * There are still some fine points to be ironed out in main jEdit and some > plugins, i.e. bad GUI rendering on very high resolution displays. > > This means there will be a few small changes to the jedit_build > components, based on what the official jEdit project provides in the > coming weeks. This will not include any of my changes as no one has looked at my patches to jEdit since however many months ago I submitted them. > Concerning the font substitution approach: Did you rethink my proposal > to use the python interface of fontforge to assemble Isabelle font > derivatives systematically? So, concerning this situation, you are right and the correct way to go about font substitution is not to do it, or do it offline. Java's font substitution system is too poor to do what we want without massive effort. I am looking at the python+fontforge route, but making slow progress so far due to work commitments interrupting. However, that does not change the fact that your way of splitting chunks into little pieces every time you encounter an Isabelle symbol is inefficient. The patch I sent out in "Font substitution and handling in Isabelle/jEdit" on the 3rd of September contains a change, along with a small change to jEdit to expose some extra information. As I already stated multiple times in the past, that change needs to address font substitution because font substitution is a feature in jEdit. If someone enables it, then your rendering of chunks must still match up with jEdit's rendering of chunks, because you are overlaying one on the other. You currently split the chunks needlessly and use lots of IDs regardless of font substitution being enabled or not. With my change, font substitution still works, sure, but the important thing is it renders the entire jEdit chunk with a single call when font substitution is disabled. This simplifies memory layout and rendering code in the most common case which is the only case you want to support (i.e. everyone using IsabelleText font only). I really cannot say anything more unless you look at the patch I sent and see how the code changes. I don't know why that is not possible. > This would allow applications to use just one font. Thus the special > tricks of the jEdit text area won't be required. The result would also > work with plain Java Swing components, or in a completely different GUI > context (e.g. a web browser). Yes, and if you rip out font substitution from jEdit entirely, then my patch to rendering simplifies even more. > Note that the Isabelle-generated HTML pages already include the Isabelle > fonts since Isabelle/b3c665940d62 (and a few later changes). Other > fonts could be used as well, by modifications in the CSS. > > Thus we have a chance to get a uniform approach to Isabelle symbol > fonts, generated offline by some administrative python script. Sure, and generating these fonts offline will allow crazy people like me to have their own font which still includes all the glyphs necessary, satisfying both you and I. I will spend some evenings this week looking at scripting fontforge to generate IsabelleText. Could you please take a little while to look at my changes? I'm completely open to the idea of you not liking them and requesting further changes or rejecting them, but endless discussion without even looking really seems a waste of time. If no one looks at anything I do, then I can just keep a local fork going and keep quiet about the changes. Either way, I am not bringing this change up any more after this email, and consider it "rejected without consideration", along with the jEdit patches I submitted. For the record, all changes are still running along without any problems months later, and have been stress tested by working on the largest parts of the L4 verification project. Sincerely, Rafal Kolanski ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On 15/09/15 05:57, Makarius wrote:
> On Tue, 25 Aug 2015, Rafal Kolanski wrote:
>
>> - Removes hardcoded colors in favor of looking up relevant JEdit
>> properties. This is critical if you want a light-on-dark setup.
>> Also in patches/extended_styles style[0] is hardcoded to black
>> in org/gjt/sp/util/SyntaxUtilities.java. This should really look
>> up the view.fgColor property in JEdit!
>>
>> Generally, defaulting to BLACK for foreground is inflexible, use:
>> jEdit.getColorProperty("view.fgColor")
>> same for 255,255,255 for a background, try use:
>> jEdit.getColorProperty("view.bgColor")
>
> I wonder where this strange light-on-dark trend is coming from, maybe
> from mobile devices? Many decades ago, monitor display quality was too
> poor for proper black-on-white text, which is why I consider this as
> luxory.
I can't speak for everyone, but my colleagues will attest to the fact
that my eyes are strange. I run my screens with 50% brightness,
light-on-dark and use custom stylesheets to recolor most of the internet
to be black-on-grey. You are right, and studies show this, that
white-on-black yields the highest contrast ratio and best readability.
Unfortunately, for people like me that effect lasts 15 minutes and then
I need to stop. With my current setup, even after 12 hours, my vision
doesn't get blurry at the end of the day. So it isn't purely aesthetic.
As for phones, they're going away from light-on-dark too (e.g. Android
Lollipop).
> Anyway, hardwired values are bad. I've changed most of them in
> 1d9c121cbe4d and 9791f631c20d.
Agreed, and thank you.
> The patched jedit code base will be updated again for the coming release
> of 5.3.0, which should appear *really*soon*now*. It will be the first
> jEdit release with proper 4K display support!
Well, I hope they have time take a peek at some of the patches sitting
in the queue before then...
Sincerely,
Rafal Kolanski
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On 15/09/15 01:15, Makarius wrote: > On Tue, 25 Aug 2015, Rafal Kolanski wrote: > >> There is no separate symbol font setting, but JEdit does supply a nice >> cascading font substitution system (if glyph not found in main font, >> try next, then next, until optionally try every one in the system). It >> even lets you specify font sizes so their metrics match! > >> The Isabelle plugin doesn't use it. > > This font-replacement mechanism is a relatively recent addition to jEdit > from a few years ago. The Isabelle/jEdit treatment of symbols, fonts, > text rendering preceeds that by 1 or 2 years. When the jEdit guys added > that feature, I noted it down on my TODO list immediately to revisit my > own approach. So far it did not happen for various reasons: > > * Font replacement only affects text area derivatives. For basic GUI > components it does not have any effect. We have some ugly tricks like > using HTML and IsabelleText font in some places, e.g. Sidekick entry > titles. Relying too much on font replacement would render that even > worse relatively to the text area. I hope you have time to take a look at my suggestion (jEdit patch submitted upstream plus changes to Isabelle/jEdit rendering posted to the list on the 3rd of September). It addresses the issue of matching jEdit's substitution during rendering text area derivatives, and reduces chunk-splitting significantly. For basic components I do not presently have a solution. GTK2/3 just does a system-wide search to find missing glyphs, and Qt plugs into that, but the JDK doesn't. Maybe someday. > * The jEdit "Chunk" concept (text tokens to be rendered eventually) is a > bit odd. Looking myself too closely at it has a real danger of > spending a lot of time there to rework it. I still want to do it > someday, but it does not have top priority at the moment, in contrast > to things like proper GUI scaling (for "4K" displays on Windows and > Linux). I have not used jEdit long enough to decide how well the concept is executed, but the "chunk" setup seems not unusual for modern editors. If you were to do it again, which approach would you prefer? > * Java 6 on Mac OS X had its own super-smart font-replacement, and my > main work machine at that time was that platform. A bit too many > problems with such not-fully-working add-ons descreased the priority > further. Now we have standard Java 8 even on Mac OS X, and it > probably does not get in the way anymore, but I did not check it. On Linux (Ubuntu), I have not seen any form of font-replacement happen on the JDK for at least Java7/8. I do not recall it happening ever, so it may be a special OS X tweak. > [...] >> The lookup system then depends on compressing a maximum of two fonts >> plus other meta information (subscript, superscript, bold) for every >> JEdit chunk type (19 types) into a single Java byte... which is >> signed, so 127 tags is maximum. Is this done for speed? > > Presumed "speed" is a lame reason for anything. I guess that Slava > Pestov simply did not know better when he made that many years ago. > There are a few more oddities at the bottom of text area and buffer > management, e.g. odd "split arrays" taken from Emacs. Without thise > mutable data non-sense -- with bytes, chars, arrays at the bottom -- > jEdit could be much faster and more scalable. This is a misunderstanding, the question was referring to why you did it that way, and after doing the work to implement the font substitution functionality, I understand now (and tried to document it as best I could in my long post on fonts/rendering). jEdit is strange to me in various ways. The type questions I get is "hey Raf, can you make parenthesis highlighting work in the output buffer?", or "why can't we pop over to the output/query window and select stuff with keyboard?". The answer is "not without modifying jEdit to add a virtual EditPane that allows sending keystrokes to a text area that isn't in an EditPane, otherwise jEdit will send it to the last active EditPane even though it's not focused" etc. >> It's a bit of a shock to new users that after they specify their fonts >> the way they like, when JEdit loads everything looks great for a few >> seconds, and then most symbols turns to rectangles when the Isabelle >> plugin loads. > > I doubt that new users will specify fonts "the way they like". jEdit is > so flexible, that it can be configured in ways that Isabelle/jEdit no > longer works properly. We ship sane defaults, with a clear bias to > support one standard way that works well. Even just that is already > difficult to maintain. I know you are hes
Re: [isabelle-dev] Fonts in etc/symbols with space in the name (incl. workaround for Isabelle-2015), patch thoughts
On 03/10/15 00:35, Makarius wrote: > On Tue, 15 Sep 2015, Rafal Kolanski wrote: > >>> The patched jedit code base will be updated again for the coming >>> release of 5.3.0, which should appear *really*soon*now*. It will be >>> the first jEdit release with proper 4K display support! >> >> Well, I hope they have time take a peek at some of the patches sitting >> in the queue before then... > > Right now I hope the jEdit guys will finally release the "Spring 2015" > version before the winter comes on the northern hemisphere. > > jEdit 5.3.0 was planned to appear early June 2015. This summer I added > various things on top of the repository version, expecting it to be > post-release material, but they actually started picking it up after a > few weeks and added most of it to the release branch. This caused > further delays. > > My priority at the moment is to see a release of jEdit, before we enter > the critical release phase for Isabelle2016 -- presumably at the start > of the Winter season here in the north. My patches to jEdit are pretty simple, but I understand if they only have a chance to be looked at after the release. > Once it is there, I will update the jedit_build component accordingly. > Then we have a brief window of opportunity to add some small patches on > top of the standard jEdit code base as part of the Isabelle distribution. Well, if you're already warning me that the window will be very small if and when it happens, then I would like to endeavor to make it count. Please consider that while you might not be able to take the patch now, you can use my time between now and then to make improvements. If you find yourself with some spare cycles, perhaps you can do a Linus and take a look at my patch to Isabelle's font rendering to see if you like at all as a concept (there's a nice simplification to the rendering code in there in addition to the font substitution). If so, I can do extra work to make it more palatable to you / the Isabelle code base. If you don't like it, fair enough, and I'll just maintain a branch locally for my colleagues to use. In particular, since my patch allows us to have multiple levels of sub/superscript (yes, only two, but still), perhaps you would like to see that in action before we put it in? Or some other way I can assist? Sincerely, Rafal Kolanski ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal
Isabelle Developers,
While looking at Isabelle 2018, we have noticed that the ISABELLE_OUTPUT
environment variable functionality has been removed.
We have previously used this functionality for the following scenarios:
- networked home directory storing Isabelle settings, but heaps built on
a different, faster / not backed up drive
- checking out two revisions of the same repository and building them
with the same settings and version of Isabelle, or running them
side-by-side on the screen
- appending extra information from the environment to ISABELLE_OUTPUT,
allowing us to build the same repository at the same revision with
different environments (e.g. using L4V_ARCH to select the
target architecture for seL4 verification) and caching the images
The common thread between these scenarios is that the settings we use
are nearly identical, with ISABELLE_OUTPUT being the variance.
Using separate ISABELLE_HOME would be overkill.
A typical setting of ISABELLE_OUTPUT/ISABELLE_PATH we use here is:
USER_HEAPS=${OVERRIDE_USER_HEAPS:-"$ISABELLE_HOME_USER/heaps-${L4V_ARCH}${ISABELLE_HOME//\//-}"}
ISABELLE_OUTPUT=${OVERRIDE_ISABELLE_OUTPUT:-"$USER_HEAPS"}
ISABELLE_PATH=${OVERRIDE_ISABELLE_PATH:-"$USER_HEAPS"}
What is now the canonical way of supporting the workflows I described
above without having to duplicate most of etc/ jedit/ and contrib/ now
that both ISABELLE_PATH and ISABELLE_OUTPUT are gone?
Sincerely,
Rafal Kolanski
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Clarification on ISABELLE_OUTPUT env variable removal
On 28/06/18 05:27, Makarius wrote:
> On 25/06/18 06:45, Rafal Kolanski wrote:
>>
>> While looking at Isabelle 2018, we have noticed that the ISABELLE_OUTPUT
>> environment variable functionality has been removed.
>
> This refers to
>
> changeset: 68219:c0341c0080e2
> user:wenzelm
> date:Sat May 19 15:45:45 2018 +0200
> description:
> clarified store directories;
> discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT;
>
>
>> A typical setting of ISABELLE_OUTPUT/ISABELLE_PATH we use here is:
>>
>> USER_HEAPS=${OVERRIDE_USER_HEAPS:-"$ISABELLE_HOME_USER/heaps-${L4V_ARCH}${ISABELLE_HOME//\//-}"}
>> ISABELLE_OUTPUT=${OVERRIDE_ISABELLE_OUTPUT:-"$USER_HEAPS"}
>> ISABELLE_PATH=${OVERRIDE_ISABELLE_PATH:-"$USER_HEAPS"}
>
> This example already motivates the change: ISABELLE_OUTPUT and
> ISABELLE_PATH were somehow duplicates, with subtle differences. Together
> with the "system build mode" (option -s of "isabelle build", "isabelle
> jedit" etc.) it has lead to an ill-defined situation.
Agreed, ISABELLE_PATH and ISABELLE_OUTPUT were confusing.
> I have now refined the change further in
>
> changeset: 68523:ccacc84e0251
> user:wenzelm
> date:Wed Jun 27 20:31:22 2018 +0200
> description:
> clarified settings -- avoid hard-wired directories;
> tuned documentation;
>
>
> I.e. you can use ISABELLE_HEAPS above.
My sincere thanks for adding this, it really makes a big difference to
our workflow.
Rafal Kolanski
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
