[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Florian Haftmann]

isabelle: f1b257607981 tip
afp: 1a688183b05a tip

Any idea what is going on here?

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Running ConcurrentGC ...
Running MonoBoolTranAlgebra ...
Running Presburger-Automata ...
Running Vickrey_Clarke_Groves ...

MonoBoolTranAlgebra FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/MonoBoolTranAlgebra)

Output written on root.pdf (20 pages, 176819 bytes).
Transcript written on root.log.

*** Failed to apply proof method (line 465 of "/mnt/home/haftmann/data/tum/afp/master/thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy"):
*** goal (3 subgoals):
***  1. !!xa. [| ALL xa. x xa <= xa;
***  x : disjunctive.disjunctive op \ op \
***   (%f. f);
***  x \ = x xa \ x (- xa) |]
***   ==> x (- xa) <= \
***  2. !!xa. [| ALL xa. x xa <= xa;
***  x : disjunctive.disjunctive op \ op \
***   (%f. f);
***  x \ = x xa \ x (- xa) |]
***   ==> - xa \ xa <= x xa
***  3. !!xa. [| ALL xa. x xa <= xa;
***  x : disjunctive.disjunctive op \ op \
***   (%f. f) |]
***   ==> x \ = x xa \ x (- xa)
*** At command "apply" (line 465 of "/mnt/home/haftmann/data/tum/afp/master/thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy")

Vickrey_Clarke_Groves FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/Vickrey_Clarke_Groves)

***   real
***(setsum
***  (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) aa)
***   < real
***  (setsum
***(summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) a)
***   x <= real (card G)
***   0 <= x
***   (x = 0) = (a = aa)
*** goal (1 subgoal):
***  1. x <= real (card G) &
*** 0 <= x &
*** (x = 0) = (a = aa) &
*** (aa ~= a -->
***  setsum
***   (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G) aa
***  < setsum
*** (summedBidVector (pseudoAllocation a <| (N <*> finestpart G)) N G)
*** a)
*** At command "by" (line 985 of "/mnt/home/haftmann/data/tum/afp/master/thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy")
*** Timeout
Presburger-Automata FAILED
(see also /mnt/home/haftmann/data/tum/isabelle/master/heaps/polyml-5.5.3_x86-linux/log/Presburger-Automata)

  assumes "rquot_DFS A n"
Found termination order: "(%p. size_list size (snd p)) <*mlex*> {}"
Found termination order:
  "(%p. size (snd p)) <*mlex*> (%p. size (fst p)) <*mlex*> {}"
### Ignoring duplicate rewrite rule:
### accepts ?tr1 ?P1 ?s1 ?as1 == ?P1 (foldl ?tr1 ?s1 ?as1)
### Legacy feature! Bad case "goal1" (line 3660 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal2" (line 3668 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal3" (line 3672 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal4" (line 3681 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal5" (line 3685 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal6" (line 3689 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal1" (line 4057 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal2" (line 4065 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### theory "Presburger_Automata"
### 21.954s elapsed time, 75.748s cpu time, 14.988s GC time
### Legacy feature! Bad case "goal3" (line 4069 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal4" (line 4078 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal5" (line 4082 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead
### Legacy feature! Bad case "goal6" (line 4086 of "/mnt/home/haftmann/data/tum/afp/master/thys/Presburger-Automata/Presburger_Automata.thy") -- use proof method "goal_cases" instead

Re: [isabelle-dev] Future of permanent_interpretation

[Florian Haftmann]

For further discussion, see now fd4ac1530d63, particulary
src/Pure/Isar/interpretation.ML and 5.7.3 »Locale interpretation« in
*isar-ref*.

This goes along the following lines:

* »Interpretation« in general is used as generic heading for every kind
of intepretation into different destination contexts.
* *interpretation* in particular denotes interpretation into a confined
context. (The wording in the implementation is not yet consistent,
ranging from »epheremal« to »confined«; I have a slight inclination to
stick to the latter). *interpret* is the variant for proof blocks. This
use of terminology IMHO is consistent with typical uses in mathematics
and there had been little debate about that so far.

So far for the seemingly non-controversial matter.

Concerning the »persistent« / »permanent« / »subscribing« kinds of
interpretation, there are two conflicting views so far:

* Each local theory can »subscribe« to locales, given that it underlying
target implements it. Hence all targets (particularly, global theories
and locales) are treated uniformly, using one keyword
*permanent_interpretation.*
* The user interfaces emphasizes the non-trivial differences between
»subscription« into global theories and into locales, particularly the
side effects of the latter on the existing locale hierarchy.

Personally I have no strong inclination to follow the one or the other
and I am happy to abandon the first in favour for the second. However
then I also suggest a dedicated keyword for interpretation into global
theories:
a) *interpretation* would otherwise be strangely overloaded, allowing
mixin definitions on the level of global theories but not in other local
theories.
b) Conceptually it would also be possible to allow »subscribing«
interpretation into global theories inside a nested local theory
(although it is not clear whether our current implementation is actually
suitable for that). Then *theory* … *context* … *begin … interpretation*
would be ambiguous.
c) Similarly, also a theory itself can be seen as a confined context
block, making *theory* … *interpretation* itself ambiguous.
Suitable candidates could be *theory_interpretation *or
*global_interpreation*. Better suggestions welcome. Of course, the
actual replacement would not occur in the upcoming but a later release.

On that single matter I want to excite some feedback before continuing.
Also suggestions on 5.7.3 »Locale interpretation« in *isar-ref* are welcome.

Cheers,
Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.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

Re: [isabelle-dev] code abbreviation for mapping over a fixed range

[Florian Haftmann]

See now 9a51e4dfc5d9.

Florian

Am 12.11.2015 um 10:58 schrieb Jose Divasón:
> Hi Bertram, Christian and Bertram,
> 
> I would like to put my two cents in this topic. I have done a simple
> experiment about this using my AFP entry about the QR decomposition,
> where a strong use of map_range is done.
> 
> With the current map_range definition, the computation of the QR
> decomposition of a 60x60 real matrix takes about 45 seconds. However, if
> one adds the definition proposed by Bertram then the same computation
> takes about 2.43 seconds. So it really seems to be so much faster.
>  
> Best,
> Jose
> 
> 2015-11-12 10:09 GMT+01:00 Florian Haftmann
>  >:
> 
> > The new definition actually causes *more* allocation than the original
> > one, except for very short lists, because every call of @ copies its
> > first argument. Note that the code equation for [_..<_] is
> >
> >   lemma upt_rec[code]: "[i..
> > which has no calls to @ at all; a corresponding code equation for
> > a fused "map_upt f i j = map f [i.. >
> >   "map_upt f i j = if i < j then f i # map_upt f (Suc i) j else []"
> >
> > which could be used to define map_range:
> >
> >   "map_range f n = map_upt f 0 n"
> 
> OK, I'll revert this.
> 
> Thanks for having an eye on that.
> 
> Florian
> 
> --
> 
> PGP available:
> 
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de 
> 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.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

Re: [isabelle-dev] the function "real"

[Florian Haftmann]

>> There are a great many examples of theorems involving various coercion
>> functions and the relations =, <, <=. In a number of cases, the “real”
>> versions were declared as [iff]-rules, while the “of_nat/of_int”
>> versions were declared as [simp]-rules only. When identifying the two,
>> I decided it would make sense to go for iff, for maximum automation,
>> but I now think this was a mistake. I’m trying the alternative right now.
> 
> Same here. I avoid modifications of the claset as much as possible these
> days because it can lead to proof searches going astray although the
> goal had nothing to do with those modifications.

I have made similar experiences when trying in vain to turn INF and SUP
into abbreviations.

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.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] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Gammie]

Hi,

Can someone please apply the attached patch to Isabelle for me?

It does three things:
- generalises Imperative_Quicksort to work on linearly-ordered, 
heap-representable types, and not just nat
- renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist
- mildly weakens the assumptions of lemma subarray_append in theory Subarray

The first may require existing theories to add type annotations. If this is a 
concern then perhaps the right thing to do is introduce new names for the 
polymorphic operations and preserve the existing ones, but I think that is 
overkill.

The second may also break existing theories but I do not know how to otherwise 
get around having two theories with the same name.

thanks,
peter


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

[Peter Gammie]

… and this time with the patch …

> On 15 Nov 2015, at 22:15, Peter Gammie  wrote:
> 
> Hi,
> 
> Can someone please apply the attached patch to Isabelle for me?
> 
> It does three things:
> - generalises Imperative_Quicksort to work on linearly-ordered, 
> heap-representable types, and not just nat
> - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist
> - mildly weakens the assumptions of lemma subarray_append in theory Subarray
> 
> The first may require existing theories to add type annotations. If this is a 
> concern then perhaps the right thing to do is introduce new names for the 
> polymorphic operations and preserve the existing ones, but I think that is 
> overkill.
> 
> The second may also break existing theories but I do not know how to 
> otherwise get around having two theories with the same name.
> 
> thanks,
> peter



Imperative_HOL.patch
Description: Binary data

-- 
http://peteg.org/

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Andreas Lochbihler]

MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal 
of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but 
just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016. 
Presburger-Automata had a looping call to simp which looks related to the changes with 
real. It should work now in AFP/935a90e010a2.


Vickey_Clarke_Groves looks related to the changes to "real", but I have not 
tried to fix this.

Best,
Andreas

On 15/11/15 10:38, Florian Haftmann wrote:

isabelle: f1b257607981 tip
afp: 1a688183b05a tip

Any idea what is going on here?

Florian



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
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

[Makarius]

On Sat, 3 Oct 2015, Rafal Kolanski wrote:

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.


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.


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.


I have lost track of the status of this thread, with its various 
side-threads on isabelle-users, isabelle-dev, and private mail.



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.



Concerning the font substitution approach: Did you rethink my proposal to 
use the python interface of fontforge to assemble Isabelle font 
derivatives systematically?


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).


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.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] CGSCreateKeyboardEvent

[Makarius]

Larry,

I am forwarding this to isabelle-dev since more people might have seen it.

From a distance it looks to me like a problem of jdk-8u66, but Google does 

not know anything about it yet.

The Isabelle2016 release is timed to happen shortly after the next jdk-8 
release.  This gives that small garage firm called "Oracle" a chance to 
make things work more smoothly.



Makarius

-- Forwarded message --
Date: Tue, 3 Nov 2015 12:48:12 +
Subject: CGSCreateKeyboardEvent

Saw this again today
Larry

~/isabelle/Repos/src/HOL: isabelle jedit -l Pure  Real.thy
Nov  3 12:32:16  java[12869] : The function ‘CGSCreateKeyboardEvent’ is 
obsolete and will be removed in an upcoming update. Unfortunately, this application, 
or a library it uses, is using this obsolete function, and is thereby contributing to 
an overall degradation of system performance. Please use 
`CGSCreateKeyboardEventOfLength' instead.
~/isabelle/Repos/src/HOL:___
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

[Rafal Kolanski]

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] Isabelle/jEdit - Sidekick

[Makarius]

On Tue, 10 Nov 2015, Mathias Fleury wrote:

in the sidekick there is a "sub-panel"^1 below the sidekick (see the red 
rectangle in the joint screenshot). Is there a way to have line breaks 
in it? The difference between it and the tooltips that appear in the 
sidekick, is that the tooltips disappear, when moving the cursor, while 
the content of the "sub-panel" does not.


^1 it is probably not its real name, but I haven't found a better one in 
the Isabelle/jedit manual,


I think it is called "status window", as can be seen in the little options 
dialog of Sidekick.



PS: I am posting to the dev mailing list, since the jEdit version 
changed since the 2015 release, but there are no line-breaks either in 
the stable version.


SideKick did not change much in the update to jedit-5.3.0 and 
jedit_build-20151023 in Isabelle/d40f906bb13f.


Posting on isabelle-dev instead of isabelle-users means there are less 
people who might potentially join into a movement to brush up some jEdit 
components.


The real work on it needs to happen on 
http://sourceforge.net/projects/jedit though, with its various trackers 
and mailing lists.  The process is relatively slow, but it moves on 
nonetheless.  I have myself added a fair amount of changes to jEdit and 
its plugins already.



Makarius
___
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

[Rafal Kolanski]

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