Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Thomas Sewell]

"Unable to increase stack" is one of the various messages that tells you that 
PolyML has run out of resources. It doesn't really tell you what the problem is 
though. It might be an actual problem or a temporary problem caused by a 
machine being overloaded.

Cheers,
Thomas.

On 2019-03-12 12:14, Lawrence Paulson wrote:
Does anybody know what this is?

01:58:19 Running HOL-Quickcheck_Benchmark ...01:58:20 HOL-Quickcheck_Benchmark: 
theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Base01:58:20 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Find_Unused_Assms_Examples01:58:23 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Guided_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_No_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Unguided_Attacker_Example02:12:01 
Warning - Unable to increase stack - interrupting thread02:12:01 *** 
Interrupt02:12:01 HOL-Quickcheck_Benchmark FAILED

Larry

> Begin forwarded message:
>
> From: Isabelle/Jenkins 
> Subject: [Isabelle-ci] Build failure in Isabelle (benchmark)
> Date: 12 March 2019 at 01:22:32 GMT
> To: 
> isabelle...@mail46.informatik.tu-muenchen.de
>
> The Isabelle build failed. See the log at: 
> https://ci.isabelle.systems/jenkins/job/isabelle-nightly-benchmark/887/
> ___
> Isabelle-ci mailing list
> isabelle...@mail46.informatik.tu-muenchen.de
> https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci

___
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] Support in `isabelle build` for SOURCE_DATE_EPOCH

[Thomas Sewell]

Apologies, I forgot about this discussion and just now remembered it.


It sounds like this feature might be quite valuable to projects like 
l4.verified with fairly "heavy" sessions.


I'm not on that project any more, but perhaps someone there will have time to 
investigate whether everything

can be set up so that the right Path.smart_implode events happen, and perhaps 
whether it's easy to

set up a check that this happens.


Cheers,

Thomas.


From: Makarius 
Sent: Friday, November 30, 2018 10:18:12 PM
To: Thomas Sewell; Jonathon Fernyhough; 
isabelle-...@mail46.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

On 30/11/2018 21:56, Makarius wrote:
> On 30/11/2018 19:45, Thomas Sewell wrote:
>
> I am also unsure why "archive formats" got on this thread. The heap is a
> binary build artifact, with its own internal structure. Its precise
> content is somewhat non-deterministic, even when everything runs in
> sequential mode (which is very slow and hardly ever done).
>
> It works due to some special trickery for the main Isabelle sessions
> (and in Isabelle2018 also for AFP) via Path.smart_implode, to fold
> physical file locations back into symbolic form: $ISABELLE_HOME/src/...
> or $AFP/...

Another side-remark: Poly/ML does store an absolute path for the
imported heap hierarchy, but Isabelle/ML ignores that: it uses freshly
resolved file names with PolyML.SaveState.loadHierarchy. Only the
logical session name and the SHA1 key is taken into account for
dependency management.

I've confirmed that with my experiment: using the "strings" tool on the
heap file yields precisely one file name in my own home directory (where
everything was built): it is the (unused) physical heap file name
(before moving the whole installation).

[All of this with official Isabelle2018 -- and all this discussion
properly belongs to the isabelle-users mailing list. There is no mailing
list for "packaging of Isabelle for Linux distributions".]


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

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

[Thomas Sewell]

I'd just like to confirm that other users have seen this issue. Colleagues of 
mine

have tried to pre-build heaps on a build server and share them with other

users. It could have saved CPU-hours, and in some cases, hours of humans

waiting around, but it never worked.


My understanding is that the "hash the world" mechanism for capturing

the state of the dependencies sometimes captures the absolute names of files.

This breaks down in the obvious way if, for instance, we can't assume that all

the target users have the same username. None of this has anything to do

with the archive format.


These observations may all be out of date.

Cheers,
Thomas.



From: isabelle-dev  on 
behalf of Makarius 
Sent: Friday, November 30, 2018 7:13:36 PM
To: Jonathon Fernyhough; isabelle-...@mail46.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

On 30/11/2018 18:56, Jonathon Fernyhough wrote:
>>
>>> However, a Debian packaging file is the correct approach for local
>>> deployment to multiple Debian/Ubuntu machines.
>>
>> It is one approach, but typically causes problems.
>
> Given the size of the Debian repositories and the range of software they
> make available I'm not really sure this is true.

Hopefully this is not another attempt at an official Debian package of
Isabelle. Many years ago, some people tried it, but it always caused
more problems than it solved. And today the system is more complex and
more easily destroyed by packaging it.

These days I see big and complex products doing it our way: providing a
fully integrated distribution for end-users that by-passes OS package
managers.


Makarius

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

Re: [isabelle-dev] next release

[Thomas Sewell]

OK, I'll respond to these points in-line.


A discussion without sources to look at is difficult.


OK, I attach my working version. Colleagues of mine were told off
recently for producing patches without the relevant authority, so these
days I begin these discussions in abstract. Feel free to tell me that
I'm doing it wrong some new way.


Generally, these hooks are rather old, predating the managed
evaluation of the PIDE document model.  There used to be more hooks in
ancient times, but we have managed to get rid of most of them.


OK. I'm not familiar with the history. What I'm proposing is somewhat
orthogonal to the document model as I understand it though. Sure,
essential parts of the system/protocol should be built in rather than
"hooked" in. But rarely used add-on features can be more cleanly
supported by small "hooks" than by building e.g. mirabelle directly into
the system toplevel.


The general plan (for many years already) is to unify the batch build
mode further with the managed evaluation of PIDE interaction.  In
particular there should be proper ways to fork (and maybe ignore)
proofs in the document model.  Odd flags like skip_proofs or
quick_and_dirty/sorry might eventually disappear.


Such a consolidation might be nice, though obviously the performance
implications have to be managed. Some of these add-ons could perhaps
observe the proofs being done from the Isabelle/Scala side. Is that what
you're getting at? It sounds a bit involved.


As usual there is a conflict of proper principles done right, and
small adhoc patches to an already complex system.


However, doing things right seems to take a long time. Empirically,
fiddling with skip_proofs etc allows some users to see a 2-3x
improvement in their productivity. The question is just how official
this fiddling is allowed to be.

Cheers,
Thomas.




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
diff --git a/src/Pure/Isar/proof.ML b/src/Pure/Isar/proof.ML
index 961a582..9b158be 100644
--- a/src/Pure/Isar/proof.ML
+++ b/src/Pure/Isar/proof.ML
@@ -504,7 +504,11 @@ fun conclude_goal ctxt goal propss =
 val finished_goal_error = "Failed to finish proof";
 
 fun finished_goal pos state =
-  let val (ctxt, (_, goal)) = get_goal state in
+  let
+val (ctxt, (_, goal)) = get_goal state
+val _ = if Thm.no_prems goal then Goal.run_finish_hooks
+"Proof.finished_goal" ctxt goal else ()
+  in
 if Thm.no_prems goal then Seq.Result state
 else
   Seq.Error (fn () =>
diff --git a/src/Pure/Isar/toplevel.ML b/src/Pure/Isar/toplevel.ML
index c31e3ce..b889b6f 100644
--- a/src/Pure/Isar/toplevel.ML
+++ b/src/Pure/Isar/toplevel.ML
@@ -459,7 +459,9 @@ fun begin_proof init = transaction (fn int =>
   (fn Theory (gthy, _) =>
 let
   val (finish, prf) = init int gthy;
-  val skip = Goal.skip_proofs_enabled ();
+  val skip = case try Proof.goal prf of NONE => false
+| SOME goal => Goal.skip_goal "Toplevel.begin_proof"
+(#context goal) (#goal goal)
   val schematic_goal = try Proof.schematic_goal prf;
   val _ =
 if skip andalso schematic_goal = SOME true then
diff --git a/src/Pure/goal.ML b/src/Pure/goal.ML
index d0d3d74..fddbf5e 100644
--- a/src/Pure/goal.ML
+++ b/src/Pure/goal.ML
@@ -23,6 +23,10 @@ sig
   val finish: Proof.context -> thm -> thm
   val norm_result: Proof.context -> thm -> thm
   val skip_proofs_enabled: unit -> bool
+  val skip_goal: string -> Proof.context -> thm -> bool
+  val add_skip_hook: (string -> Proof.context -> thm -> bool) -> unit
+  val add_finish_hook: (string -> Proof.context -> thm -> unit) -> unit
+  val run_finish_hooks: string -> Proof.context -> thm -> unit
   val future_enabled: int -> bool
   val future_enabled_timing: Time.time -> bool
   val future_result: Proof.context -> thm future -> term -> thm
@@ -122,6 +126,24 @@ fun future_enabled_timing t =
   future_enabled 1 andalso
 Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
 
+val skip_hooks = Synchronized.var "Goal.skip_hooks"
+([] : (string -> Proof.context -> thm -> bool) list)
+
+fun add_skip_hook h = Synchronized.change skip_hooks (cons h)
+
+fun skip_goal nm ctxt thm = skip_proofs_enabled ()
+orelse exists (fn h => try (h nm ctxt) thm = SOME true)
+(Synchronized.value skip_hooks)
+
+val finish_hooks = Synchronized.var "Goal.finish_hooks"
+([] : (string -> Proof.context -> thm -> unit) list)
+
+fun add_finish_hook h = Synchronized.change finish_hooks (cons h)
+
+fun run_finish_hooks nm ctxt thm = List.app (fn f => (try (f nm ctxt) thm; ()))
+(Synchronized.value finish_hooks)
+
+fun finish_hook_tac nm ctxt t = (run_finish_hooks nm ctxt t; Seq.single t)
 
 (* future_result *)
 
@@ -181,7 +203,8 @@ fun prove_common ctxt fork_pri xs 

Re: [isabelle-dev] next release

[Thomas Sewell]

I have two items of interest for the coming release.

There is some interest here at Data61 (NICTA that was) in having a
localised record package in Isabelle-2016. I've done the initial
implementation and got the parts of the package I understand working
within locales etc, but something goes wrong with the code generation
aspect. Is there anyone who understands how to debug the code generator
who'd have time to look at that?

The second proposal is probably more contentious. I'm hoping to
reimplement a tool we had in the past that speeds up proof maintenance
work by selectively skipping proofs that are very likely to succeed. To
support that, I'm proposing adding a couple of hooks to Pure/goal.ML,
similar to the hook in Pure/Isar/toplevel.ML. One hook will allow the
tool to install an oberver (context -> thm -> unit) for completed
proofs. Another (context -> thm -> bool) will allow the tool to observe
proofs as they commence, and to optionally recommend they be skipped.

This second change essentially just gives the user a little more
control, they could skip the proofs with skip_proofs anyway. Still, I'm
sure it will provoke some interesting discussion.

Cheers,
Thomas.

On 14/01/16 02:55, Lawrence Paulson wrote:

I don't expect to contribute anything else before the next release. There are 
little bits that I could add, but probably I should desist in the name of 
stability.

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





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Thomas Sewell]

I've had a quick scan over the NICTA repositories. It doesn't look like
there are any live original uses of recdef. There are recdefs in a copy
of Simpl-AFP, and in some backups of historical papers.

Short summary, NICTA doesn't have any stakes in recdef.

Cheers,
Thomas.

On 08/06/15 06:13, Makarius wrote:

On Sat, 6 Jun 2015, Gerwin Klein wrote:




On 06.06.2015, at 21:23, Makarius makar...@sketis.net wrote:

 (2) 'defer_recdef' which is unused in the directly visible Isabelle
   universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter
in the Isabelle universe, where 'defer_recdef' still occurs.
Otherwise I will remove it soon, lets say within 1-2 weeks.


Unused in our part of the dark matter universe as well.


The thread has shifted over to actual 'recdef'. Are there remaining
uses of 'recdef' in the NICTA dark matter?

So far I always thought the remaining uses in HOL-Decision_Procs are
only a reminder that there are other important applications.


Makarius

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






The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Towards the Isabelle2014 release

[Thomas Sewell]

The changeset has landed in the sense that I sent Gerwin a bundle containing:

changeset:   6bf63b1f41f0
tag: tip
user:Thomas Sewell thomas.sew...@nicta.com.au
date:Wed Jun 11 14:24:23 2014 +1000
summary: Hypsubst preserves equality hypotheses

He probably pushed it to the testboard with that changeset ID, but he might 
have rebased, in which case it will have that summary but a different ID. I 
don't know what the testboard report was, and in the meanwhile Gerwin has been 
travelling, so no further progress has been made.

I'd like to get this process moving again. If noone has any objections, I'd 
like to move the change into mainline ASAP so it can be included in the 
upcoming release. I can help fix any resulting failures which I've somehow 
overlooked. I'm not sure who I should ask to push the change in though.

Thomas.


From: Makarius [makar...@sketis.net]
Sent: Monday, June 30, 2014 9:56 PM
To: Gerwin Klein; Thomas Sewell
Cc: isabelle-dev@mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Towards the Isabelle2014 release

On Wed, 11 Jun 2014, Gerwin Klein wrote:

 On 11.06.2014, at 2:56 pm, Thomas Sewell thomas.sew...@nicta.com.au wrote:

 Gerwin will push the isabelle hypsubst change to the testboard now (assuming 
 he can remember how).

 He could and did.

Has that change been landed?  Which changeset IDs are relevant?

I don't have any special expertise in this area, but merely want to make
sure that we can move on towards the release.


Makarius



The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Has anyone ever run out of memory trying to *start* to build the AFP?

[Thomas Sewell]

While fixing theories in the AFP, I arrived in a strange situation where 
isabelle build -D thys would no longer find and check the remaining 
unbuilt theories.


Instead, I got a java OutOfMemory exception on the java heap. This is 
before anything starts building - I take it java has run out of heap 
just trying to parse all the theories, logs and heaps and figure out 
what work to do.


Unfortunately I can't exactly reproduce this, since I've since got a 
theory to build and changed the outcome. Instead isabelle seems to get 
stuck - after 10 minutes at ~6 cores java still hasn't picked and 
started any sessions.


In case anyone else gets stuck in this situation, here is my best 
workaround:


cat thys/*/ROOT | grep session | cut -d' ' -f2 | xargs -n 10 isabelle 
build -d thys


By focusing on (the dependencies of) 10 sessions at a time, isabelle 
seems to get the job done.


The grepping and cutting is a bit ugly. Would it make sense to have an 
equivalent of 'findlogics' which found sessions? That would allow


isabelle findsessions -d (DIR) | xargs -n 10 isabelle build -d (DIR)

If noone else has seen this kind of thing, just ignore me.

Cheers,
Thomas.

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

Re: [isabelle-dev] Towards the Isabelle2014 release

[Thomas Sewell]

Indeed, there is a backward compatibility mode declaration. In fixing 
things, I've been trying to use it as little as possible and as locally 
as possible. Perhaps I should be bolder.


I'm aesthetically against using the compatibility mode all over the 
place, since I feel that it's just mysterious. Of course, a lot of 
Isabelle proof scripts are a bit mysterious already.


In particular, I want to avoid ever changing the setting globally. I've 
had some bad experiences in the past with theories with differing global 
configurations, which means that the location of a tactic and the 
include graphs of theories start having subtle effects on the way the 
tactics run. It's a mess.


I've started running through the AFP, and it doesn't look too bad. I'll 
report on this again in the next few days.


Cheers all,
Thomas.

On 04/06/14 23:23, Lawrence Paulson wrote:

Didn’t we agree that a “backward compatibility mode” declaration (restoring the 
former behaviour) would have to be available? That should make repairing legacy 
proofs trivial. Naturally we would like to gradually port some of these 
developments to do things the new way, but only some of them, and not 
immediately.

Backward compatibility will be necessary for users, even if not for us.

Larry

On 4 Jun 2014, at 06:27, Thomas Sewell thomas.sew...@nicta.com.au wrote:


I had hoped to have the change I was making to hypothesis-substitution ready 
for the coming release.

I've got it working for all of HOL and the library, and begun looking at the 
AFP and at the l4.verified proofs. The HOL+library changes were easy enough, 
but the l4.verified changes are somewhat daunting and I haven't gotten anywhere 
with the AFP yet.

I'll have another look at it, because I'd like this to go somewhere at some 
point. It might have to wait for a subsequent release though.

Cheers,
Thomas.

On 30/05/14 21:30, Makarius wrote:

The summer is getting close, and we need to start thinking about the coming 
release.

I am myself on vacation during most of June. On return I would like to wrap up 
rather quickly, so that we can publish Isabelle2014-RC0 in the second week of 
July, for the Isabelle tutorial at VSL2014 Vienna.  That will be still within 
the main Isabelle repository.

The usual fork to the release repository and the regular sequence of 
Isabelle2014-RC1, RC2, RC3, ... will happen in the week after ITP 2014.

I am myself attending the mega event at Vienna 13..19-Jul-2014. This will be 
also an opportunity to show me personally remaining snags, and to continue the 
elimination of remaining uses of Proof General.  (It is getting harder and 
harder to construct counter-examples to the claim that this set is already 
empty.)


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


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

Re: [isabelle-dev] Towards the Isabelle2014 release

[Thomas Sewell]

I had hoped to have the change I was making to hypothesis-substitution 
ready for the coming release.


I've got it working for all of HOL and the library, and begun looking at 
the AFP and at the l4.verified proofs. The HOL+library changes were easy 
enough, but the l4.verified changes are somewhat daunting and I haven't 
gotten anywhere with the AFP yet.


I'll have another look at it, because I'd like this to go somewhere at 
some point. It might have to wait for a subsequent release though.


Cheers,
Thomas.

On 30/05/14 21:30, Makarius wrote:
The summer is getting close, and we need to start thinking about the 
coming release.


I am myself on vacation during most of June. On return I would like to 
wrap up rather quickly, so that we can publish Isabelle2014-RC0 in the 
second week of July, for the Isabelle tutorial at VSL2014 Vienna.  
That will be still within the main Isabelle repository.


The usual fork to the release repository and the regular sequence of 
Isabelle2014-RC1, RC2, RC3, ... will happen in the week after ITP 2014.


I am myself attending the mega event at Vienna 13..19-Jul-2014. This 
will be also an opportunity to show me personally remaining snags, and 
to continue the elimination of remaining uses of Proof General.  (It 
is getting harder and harder to construct counter-examples to the 
claim that this set is already empty.)



Makarius
___
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] Notes on datatype_new list

[Thomas Sewell]

I have no particular stake in this issue, but I would think there was an 
option (c) which is to do the *opposite* of what Jasmin said about 
bringing the additional constant names etc as close as possible to 
wherever they fit:


datatype_new 'a list =
Nil ([])
  | Cons 'a 'a list (infixr # 65)

with
  set: set
  rel: list_all2
  map: map
  selectors: hd tl (default [])
for Cons hd tl
  discriminator: op = []

Or something like that, excuse my made-up syntax. That clarifies what 
the datatype really is and where the associated constants came from 
(well, a little bit) without having to introduce any funny syntax to 
fit all the relevant options into a single bit of syntax. It also keeps 
all the data in a single command, so the package can do everything with 
the canonical names at once.


That's just my ten cents worth. As I said, I have no particular interest 
in this.


Cheers,
Thomas.

On 26/05/14 19:56, Dmitriy Traytel wrote:

Am 26.05.2014 11:07, schrieb Jasmin Blanchette:

Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:


The definition of list should look like before.
I don't see how this is an option. This would result in the following 
duplicate constants:


 map_list vs. map
 set_list vs. set
 rel_list vs. forall_list2
 un_Cons1 vs. hd
 un_Cons2 vs. tl
Here are some compromise options that lighten the presentation, but 
still reusing the conveniences provided by the package (which are not 
only the constants, but also many theorems about the constants):


(a)

datatype_new 'a list =
Nil (defaults un_Cons2: []) ([])
| Cons 'a 'a list (infixr # 65)

abbreviation map ≡ map_list
abbreviation set ≡ set_list
abbreviation list_all2 ≡ rel_list
abbreviation hd ≡ un_Cons1
abbreviation tl ≡ un_Cons2

(b)

datatype_new 'a list =
Nil (defaults tl: []) ([])
| Cons (hd: 'a) (tl: 'a list) (infixr # 65)

abbreviation map ≡ map_list
abbreviation set ≡ set_list
abbreviation list_all2 ≡ rel_list

Option (a) is closest to the original definition---the only difference 
is in the annotation defining the default value of tl Nil. However, 
not using the selector requires us to use the automatically generated 
name un_Cons2, which makes this option too obscure.


My favourite (next to the current definition from the repository) is 
option (b)---giving name to the selectors makes the defaults 
annotation easy to parse. And even major functional programming 
languages support similar selector annotations (e.g. via record syntax 
for data in Haskell).


For both options we probably would change the package to generate the 
discriminator %x. x = Nil by default for nullary constructors.


Dmitriy


___
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] Remaining uses of Proof General?

[Thomas Sewell]

Thanks Makarius.

A few of us at NICTA have ported this change to our various versions of 
Isabelle and begun playing with it. It seems to improve the situation 
sometimes, though we haven't yet got a feel for when in particular it 
helps. In fact, we haven't really understood what the change does.


On 07/05/14 22:59, Makarius wrote:

On Mon, 5 May 2014, Makarius wrote:


 Users running on batteries might also want a mode that restricts all
 threads to the behaviour above.


Have you tried that with threads = 1 (there is also a special 
treatment for high-priority prints in that mode)?  So far I guess 
that most people run with defaults, without any idea of the tuning 
parameters.


See also:

changeset:   56875:f6259d6fb565
user:wenzelm
date:Tue May 06 16:05:14 2014 +0200
files:   etc/options src/Pure/PIDE/command.ML
description:
explicit option parallel_print to downgrade parallel scheduling, which 
might occasionally help for big and heavy scripts;



In principle this is an instance of the too many options syndrome, 
but here the implicit change of behaviour on 1 core is merely made 
explicit. Moreover, according to the waterbed-syndrome in its 
positive sense, it means that options added here inevitably cause 
other old/obsolete options to be removed faster.




I completely agree that having too many options is a problem. There's no 
point having them if noone knows that they're there, or which ones to 
try. That said, I think it's a good path for performance adjustments 
which might or might not be helpful. I suspect you could get away with 
adding far more options than you plan to have in the end, and keep only 
the ones that end up with a quorum of users. I'm a bit of an optimist 
though.


This sounds a bit too pragmatic and opportunistic to me.  What is 
special about print tasks anyway, apart from their priority?  The 
recent concept for asynchronous print functions makes print tasks 
rather general, and there are more automated provers or disprovers in 
that category than actual printing.


What is even more important than prints, is the main protocol thread, 
which presently needs to work against the whole farm of worker threads 
to update certain administrative structures of the document model.  If 
I knew a proper way to reduce the priority (or to pre-empt) worker 
threads for that, I would do it.  But it probably needs some work by 
David Matthews on the ML thread infrastructure.




Consider me an unashamed pragmatist. I see a similarity between 
task/thread scheduling in Isabelle and task/thread scheduling in 
operating systems. All modern operating systems are full of ad-hoc 
heuristics designed to bump up the priority of tasks that are likely to 
create I/O requests or update things for the user. A parallel make, 
for instance, will run much faster if the OS prioritises the compile 
tasks that are still reading files ahead of the ones that have begin 
compiling and computing. This keeps the disk working throughout the 
build. Windows raises the priority of in-focus windows, and Mac OS X 
pushes the audio threads of apps up to the highest priority, etcetera.


I may have misspoken with regard to print task. I guess I meant task 
that will produce output which at some point the user has directly 
requested into their output panel, query panel etc. If we see the user 
as an external resource like a hard disk, these are the tasks we need to 
front-load to keep the external task running at full capacity. I see the 
some of the other output tasks, which possibly produce counterexamples 
or which produce squiggly lines which are possibly helpful, as lower 
priority.


Preempting long-running tasks would change the tradeoffs a lot. Another 
possibility would be to introduce a yield-point (cooperative 
multitasking) which a task can execute, which will possibly cause its 
execution to be delayed in favour of a higher priority task. Adding that 
to the tactic combinators would make nearly all Isabelle workloads much 
finer-grained.


Well, those are just my thoughts. Thanks for the adjustment, I hope it 
solves our responsiveness problems.


Best wishes,
Thomas.


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

Re: [isabelle-dev] Remaining uses of Proof General?

[Thomas Sewell]

On 03/05/14 00:05, Makarius wrote:

On Tue, 29 Apr 2014, Thomas Sewell wrote:

I tried an adjustment a while ago in which I had the goal state print 
incrementally. Even if some of the subgoals took a while to print, 
you'd see the line with goal (12 subgoals) immediately, and then 
the subgoals as they were formatted. The short summary is that this 
helped a little sometimes, but I often still saw an empty Output 
panel for seconds after moving the cursor to a line that the 
continuous checker had already processed.


I strongly suspect that the print request was waiting in a queue 
somewhere. The system would become responsive again once it finished 
doing something else.


That is the normal future task farm, with its restricted worker thread 
pool.  All PIDE execution works via some Future.fork, with different 
priorities in the queue.  Proof tasks have low priority, print tasks 
have high priority. Once a task is running on some thread, it 
continues and cannot be preempted by newer tasks with higher priority.


The basic assumption is that each proof task does not run too long, 
and if it does it is something to be improved in the application to 
make it more smooth.  In contrast, Proof General makes it more easy to 
produce huge and heavy proof scripts that can be hardly handled by 
anyone else later.




Right. That seems to be the assumption that's being violated in the few 
cases where people are still keen on ProofGeneral, for instance, in 
Andreas' big complicated tactic applications.


The case where I get into trouble is in implementing a package-lite. I 
put together a collection of tactics or computations in ML blocks and 
execute them at some point in a theory via setup or ML. It's a bit like 
setting up a proper package and invoking it, but without the implied 
robustness or generality. Some of these can run for a minute or longer. 
They're the kind of computations that users might want to control.



With regard to the future task farm: This is pretty much what I'd 
expected. So we see a delay if all the available threads are executing 
tasks that take a while and are not the current print task. Adding more 
threads reduces the chance of this happening, but not much. The higher 
priority for print tasks means the delay will end as soon as any thread 
becomes available, so the more threads the faster on average that will 
happen, but without guarantees.


Let me make a proposal. I think that various users would appreciate it 
if one of the worker threads was reserved for print jobs caused by 
moving the cursor (highest priority tasks) and their dependencies 
(assuming more than one worker thread). That would hopefully make it 
easier to control the delay. If the user is cautious with moving the 
cursor and if enough proof dependencies have been processed, the system 
*should* be as responsive as PG. The delay would also be mostly 
unaffected by the proof task runtime, only the print task runtimes, 
which might be easier for an advanced user to manage.


Users running on batteries might also want a mode that restricts all 
threads to the behaviour above.


As always, I have no idea how difficult that would be.



On incremental printing: it's easy to implement by generalising a 
couple of the relevant Pretty operations to produce a Seq.seq 
internally rather than a list.


That would probably violate some implicit assumptions about print 
modes, which are a slightly odd intrusion into the purity of Pretty.T.


What was the reason for incremental printing anyway?  Just performance 
for huge goal states?  There are other bottle-necks concerning that, 
and if goals really do get that big one should think about other ways 
to expose them, not by printing in the old-fashioned way.


Incrementality might have other reasons and actual benefits.  In the 
early years of PIDE I had more ambitions for that, but it caused so 
many additional problems in the document model and the GUI that I 
removed most of it for the sake of delivering something that is 
sufficiently stable to be usable in practice.


The reason for the experiment was that I was fixing some proofs 
somewhere, I forget where, which had relatively fast tactics executing 
on large, slow-to-print goals. I was probably in a context where Simpl 
was loaded, where printing is slower than usual (probably the 
print/parse translations, I've had a look and got nowhere.)


It occurred to me that I could debug some of my mistakes faster if I 
just knew whether or not the tactic I'd typed had solved a goal, and 
many more if I just saw the first goal. But the time saved is probably 
lost again adjusting the goals limit, and it's annoying to do by hand. 
Incremental output seemed like a good idea.




It looked promising initially, but then became really annoying, 
because Isabelle/jEdit or PIDE resets the Output buffer each time it 
gets more to display. So if you scroll down to look for something, 
you get scrolled back up for each time

Re: [isabelle-dev] Remaining uses of Proof General?

[Thomas Sewell]

Back to the actual technical questions.  What are the main performance 
bottle-necks here? Printing of intermediate goal states?  Or applying 
intermediate steps repeatedly?




I suspect that the problem is not that the printing or the intermediate 
calculations are taking too long. It's that printing the output the user 
wants to see is waiting on some other computation finishing, creating 
the sensation of lag.


Some evidence to back this up: I tried an adjustment a while ago in 
which I had the goal state print incrementally. Even if some of the 
subgoals took a while to print, you'd see the line with goal (12 
subgoals) immediately, and then the subgoals as they were formatted. 
The short summary is that this helped a little sometimes, but I often 
still saw an empty Output panel for seconds after moving the cursor to a 
line that the continuous checker had already processed.


I strongly suspect that the print request was waiting in a queue 
somewhere. The system would become responsive again once it finished 
doing something else. I don't think that this is to do with garbage 
collection or heap sharing - I don't recall a specific instance, but I'm 
sure I've seen this behaviour when there's been plenty of spare memory. 
Sometimes there would be purple lines in the buffer, suggesting that 
some of the worker threads were busy on other tasks, but not always.


On incremental printing: it's easy to implement by generalising a couple 
of the relevant Pretty operations to produce a Seq.seq internally rather 
than a list. It looked promising initially, but then became really 
annoying, because Isabelle/jEdit or PIDE resets the Output buffer each 
time it gets more to display. So if you scroll down to look for 
something, you get scrolled back up for each time a subgoal prints, 
which can give the sensation that the editor is fighting you. That's why 
I didn't make any effort to suggest it upstream.


I don't know if that helps. Perhaps if I run across a good demonstrative 
example I'll send it across.


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

Re: [isabelle-dev] Default simprules for division in fields

[Thomas Sewell]

This makes me realise that I may have been misunderstanding field_simps. 
I've been using it as a replacement after ring_simps disappeared a while 
ago. It always struck me as odd, since I'm nearly always in a word type, 
which is a ring but not a field.


Is it just a coincidence that field_simps usually does what I want?

Cheers,
Thomas.

On 05/04/14 03:09, Tobias Nipkow wrote:

I set up field_simps to yield a decision procedure for field equality, provided
all denominators can be proved to be 0. Hence I am sceptical if adding new rules
to it is a good idea. Florian, can you give an example where previously
field_simps was too weak but with the two additional rules it works?

Tobias

On 04/04/2014 17:37, Lawrence Paulson wrote:

A very good idea, which reduces the impact of the change on existing proofs. I 
am trying it out now.

Seeing no objections, I am quite likely to push this change later today.

Larry

On 4 Apr 2014, at 15:08, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote:


lemma divide_minus_left [simp]: (-a) / b = - (a / b)
lemma divide_minus_right [simp]: a / - b = - (a / b)”

It would be a mistake to reorient the simprules, but I am suggesting that they 
should not be declared as simprules with either orientation.

Maybe

lemma divide_minus_left [field_simps]: (-a) / b = - (a / b)
lemma divide_minus_right [field_simps]: a / - b = - (a / b)”

instead?

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


___
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] Safe approach to hypothesis substitution mark II

[Thomas Sewell]

Whoops.

It's both a typo and use of the wrong release.

The patch happens to work against Isabelle2013-1 or Isabelle2013-2, 
since there are no relevant differences in the theory sources. I can 
confirm that isabelle build -a works in either 2013-1 or 2013-2.


Short version of the story, I forgot the name of the newest release.

Long version: The confusion was caused in part because the newest 
l4.verified branch is called '2013-1'. It contains Isabelle 2013-2, but 
the switch was accomplished so straightforwardly that we didn't end up 
with a new branch name.


Apologies about the confusion,
Thomas.

On 16/01/14 02:00, Makarius wrote:

On Tue, 14 Jan 2014, Thomas Sewell wrote:


This is also a patch against Isabelle2013-1.


Is that just a typo, or are you still using that failed release? The 
current one is Isabelle2013-2, and it does not introduce any 
incompatibilities over Isabelle2013-1, so there is no reason to keep 
using that.



Makarius


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

[isabelle-dev] Can I request an improvement to the error for Duplicate session

[Thomas Sewell]

Hey Isabelle devs.

I've just spent a few minutes helping a teammate who was getting 
Duplicate session errors out of isabelle build/jedit.


To reproduce this error, take a version of isabelle at, say, 
~tsewell/work/isabelle, and attempt isabelle jedit -d . -d 
~tsewell/work/isabelle.


(Needless to say, the additional -d parameter was passed implicitly in 
my colleague's setup, or else we would have figured this out much faster.)


Anyway, this would all be a lot easier to understand if 
isabelle/src/Pure/Tools/build.scala reported both the duplicate 
specification addresses.


At enormous risk of offending the wizards of the realm by appallingly 
wasting their time, this is a patch that solves the issue:


diff -r 22d0c7fe0dfa -r 0d2b3391c1d9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scalaFri Dec 20 17:15:40 2013 +1100
+++ b/src/Pure/Tools/build.scalaMon Dec 23 13:26:55 2013 +1100
@@ -117,7 +117,9 @@
 (Graph.string[Session_Info] /: infos) {
   case (graph, (name, info)) =
 if (graph.defined(name))
-  error(Duplicate session  + quote(name) + 
Position.here(info.pos))

+  error(Duplicate session  + quote(name)
++ Position.here(info.pos)
++ Position.here(graph.get_node(name).pos))
 else graph.new_node(name, info)
 }
   val graph2 =


Cheers,
Thomas.

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

Re: [isabelle-dev] Alternative thoughts about certifying and reading input parameters to Isabelle command functions

[Thomas Sewell]

Hey Florian.

Just my two cents, but does uncurrying buy you anything here?

The function doing the actual work, do_foo in your example, has not 
been given a name and type before. So you're free to have it accept a tuple:


fun do_foo (x_1, x_2, ... x_n) = ...

And now val foo_cmd = read_foo_spec # do_foo

It's possibly a slight nuisance to someone wanting to wrap some 
parameter adjustment around do_foo, although that was probably fiddly 
anyway.


Yours,
Thomas.


On 28/04/13 00:31, Florian Haftmann wrote:

Hi all,

when Isabelle packages (in the widest sense) provide an interface to the
user, the following pattern is common practice:


fun gen_foo prep_1 ... prep_n raw_x_1 ... raw_x_n ctxt =
   let
 val x_1 = prep_1 ctxt raw_x_1;
 ...
 val x_n = prep_n ctxt raw_x_n;
   in
 ctxt
 |  ...
   end;

val foo = gen_foo cert_1 ... cert_n;
val foo_cmd = gen_foo read_1 ... read_n;

Here, raw_x_1 ... raw_x_n are unchecked arguments to the abstract
interface foo; these must be checked if provided from outside (via
cert_1 ... cert_n) or parse if fed from Isar source text (via read_1 ...
read_n).

This pattern tends to obfuscate if foo again is parametrized, see e.g.
http://isabelle.in.tum.de/repos/isabelle/file/182454c06a80/src/Pure/Isar/expression.ML#l848
ff.

I'm asking myself whether we could spend some combinators for that
problem (cf. attached file).  The idea is that two separate functions

   fun cert_foo_spec ctxt raw_x_1 ... raw_x_n = ...
   fun read_foo_spec ctxt raw_x_1 ... raw_x_n = ...

certify resp. parse their input arguments and provide the result as a
tuple.  This would be connected to the process function proper using e.g.

   val foo = cert_foo_spec #~~~  do_foo
   val foo_cmd = read_foo_spec #~~~  do_foo

The drawback is that the signatures of the combinators contain numerous
type variables, and for each arity a separate combinator is needed
(which, I guess, you cannot escape when you perform uncurrying of
arbitrary-sized tuples). Maybe it is worth some thought nevertheless.

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] Fix top-level printing of exception messages containing forced-line breaks

[Thomas Sewell]

None of us reported my problem, because it concerned a somewhat 
elaborate case in some somewhat elaborate code I wrote, which we never 
managed to conveniently reproduce. Noone realised at the time that the 
exception-printing mechanism was at fault all by itself. This would be 
an archetypal bad bug report.


By comparison, David is providing you with what would be considered a 
good bug report in most open-source communities. It comes with a clear 
explanation not only of what the problem is but what causes it to occur, 
and how it might be fixed. In such communities, the proposed patches are 
nearly never applied as-is, but they provide a far more useful starting 
point than the average bug report.


I suppose Isabelle is interesting in that it is largely deterministic, 
so if a complaint can be minimised it can usually be easily reported.


On the topic of mailing lists: we do indeed have a highly reactive 
mailing list, but many of us find that the usual reactions are rarely 
useful. We attempt to improve the quality of information in both 
directions by focusing on issues where there is a quantity of evidence. 
In particular, you do not want a running blog from me of every occasion 
on which Isabelle thwarts me.


Finally, on the issue of WWW_find, I know that Raf has had a look at 
it, and declared that it isn't a triviality. I think it might be a while 
before any serious work on it is done.


Yours,
Thomas.

On 04/04/13 21:42, Makarius wrote:


On Thu, 4 Apr 2013, Thomas Sewell wrote:

David's investigation explains a problem we had a few years ago where 
some custom tactics of mine were killing my colleagues' ProofGeneral 
sessions when they encountered errors. The workaround at the time was 
to remove all potentially useful debugging information (terms, in 
particular) from the relevant exceptions. Unfortunately this made 
tracking down the bugs in the tactics somewhat challenging.


In hindsight, I should probably put the debug terms in the 
tracebuffer and thrown a vanilla exception. Hindsight is perfect, of 
course.


So why did none of you guys ever report that?  We have a very reactive 
isabelle-users mailing list, compared to most other project's issue 
trackers.  It is also possible to discuss anything for inter-release 
Isabelle versions here on isabelle-dev, although its reactivity needs 
to be specifically slowed down to avoid hazards in the development 
process.



Having a certain observation or undesirable behaviour on someone's 
TODO list for 1-2 years already, it is like to be a matter of the past 
now.


Instead we have a lot of wasted time here with patches that are 
proposed in a way to make it an urgent and immediate issue to be 
fixed while you wait.



Makarius


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

Re: [isabelle-dev] Problem with let-simproc

[Thomas Sewell]

I'd forgotten I'd ever reported this to you.

My problems with let_simproc run a little deeper anyway, and I've moved 
to a different approach in the meanwhile. Sorry if I've left you 
labouring on my behalf.


Yours,
Thomas.

On 07/02/13 02:38, Johannes Hölzl wrote:

Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius:

On Tue, 5 Feb 2013, Johannes Hölzl wrote:


there is a bugproblem with the let-simproc, resulting in a non
terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of
isabelle-release):

  theory Scratch imports Complex_Main begin

  lemma (let x = Collect P in R x x ∧ (Ball s P)) = X
using [[simp_trace]]
apply simp

The attached hg-bundle changes this behaviour to a terminating simproc.
(The bundle can be applied to a repo containing #58e2d0cd81ae by
hg pull let_simp_betaeta.bundle)

It currently runs in the testboard:
  http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c

@Makarius: Is it possible to include this patch in Isabelle2013, when
the testboard run is green?

Testboard does not test very much, compared to what has been tested
manually and semi-automatically in the past 2 weeks for the release.  AFP
would also have to be covered.

Anyway, this behaviour of let_simproc seems to have been there from its
beginning, or at least back until Isabelle2011 (what is what I have
tried). Nobody has noticed a problem in several years, so this change is
for the next release, unless there are really strong reasons to revisit it
now.


Makarius

Thomas reported the problem to me. For me it is okay to fix it after
Isabelle2013.

@Thomas: Is it important for you to fix it in Isabelle2013? I hope the
workaround with adding Let_def to the simplifier should work fine. Then
I will add it just to the development version of Isabelle.

  - Johannes





___
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] simplifier and subgoaler not transitive

[Thomas Sewell]

Question: it looks to me like (atom v # (x, y)) = (atom v # x  atom v 
# y)


It also looks like what you're trying to do is allow the system to 
reason with the above equality without actually giving it that equality. 
It looks like you've provided the equality in one direction as a rewrite 
rule and in the other direction by adjusting mksimps (just guessing 
here, but that's what it looks like).


Did I guess right? If so, I know why that won't work :-) The new rewrite 
rules created by mksimps aren't themselves candidates for 
simplification, so the system won't apply Nominal2_Base.fresh_at_base_2 
to them, which was what resulted in further progress on goal #2.


Those are all giant guesses. Am I anywhere near the mark?

More directly, why not just add the rewrite at the top of this email to 
the simpset? This will reduce all of these sharp statements to trivial 
inequalities. This is the approach that fits with the general design of 
the simplifier. Not the structure you want? Too many inequalities? In 
that case you really need a guided solver - giving the simplifier 
opportunities for wild exploration will just slow everything down.


Yours,
Thomas.

On 23/05/12 02:23, Christian Urban wrote:

Dear All,

Assuming that this is about the bowels of the simplifier,
I hope this is the right place to ask the following question.

The simplifier has a subgoaler, which helps with rewriting
conditional lemmas. This simplifiying/subgoaling process seems
to be not transitive (probably is not meant to be). The problem
that arises for me is the following: I have set up the simplifier
to automatically solve the first two lemmas:

   lemma atom v # (x1, x2) ==  atom v # x1
   apply(simp)
   done

   lemma atom v # x1 ==  v \noteq  x1
   apply(simp)
   done

but it chokes, if I am trying to string both lemmas
together

   lemma atom v # (x1, x2) ==  v \noteq  x1
   apply(simp) --fails

Is there some magic that I can make the simplifier to
deal also with the latter goal?

The cool thing about jEdit is that I have the simplifier
traces of all three goals next to each other (the trick
is to disable the auto update). Unfortunately, I am
not very good at reading these traces. The only thing I
can say is that the simplifier starts off with goal 1
and 3 in the same direction, but then things start to
diverge. Is there a place where one can read up about
the tracing information of the simplifier? The traces
are attached for reference.

Best wishes and thanks for any help,
Christian



GOAL 1
==

  [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ (x1, x2) ⟹ atom v ♯ x1
  [1]Applying instance of rewrite rule ??.unknown:
?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯ (?x1.1, ?x2.1) ≡ True
  [1]Trying to rewrite:
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
  [2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ x1
  [1]FAILED
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
  [1]Adding rewrite rule ??.unknown:
atom v ♯ x1 ≡ True
  [1]Adding rewrite rule ??.unknown:
atom v ♯ t ≡ True
  [1]Applying instance of rewrite rule ??.unknown:
atom v ♯ x1 ≡ True
  [1]Rewriting:
atom v ♯ x1 ≡ True
  proof (prove): step 1

goal:
No subgoals!


GOAL 2
==

  [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ x1 ⟹ v ≠ x1
  [1]Applying instance of rewrite rule Nominal2_Base.fresh_at_base_2:
?a1 ♯ ?b1 ≡ ?a1 ≠ atom ?b1
  [1]Rewriting:
atom v ♯ x1 ≡ atom v ≠ atom x1
  [1]Applying instance of rewrite rule 
Nominal2_Base.at_base_class.atom_eq_iff:
atom ?a1 = atom ?b1 ≡ ?a1 = ?b1
  [1]Rewriting:
atom v = atom x1 ≡ v = x1
  [1]Adding rewrite rule ??.unknown:
v = x1 ≡ False
  [1]Applying instance of rewrite rule ??.unknown:
v = x1 ≡ False
  [1]Rewriting:
v = x1 ≡ False
  [1]Applying instance of rewrite rule HOL.simp_thms_8:
¬ False ≡ True
  [1]Rewriting:
¬ False ≡ True
  proof (prove): step 1

goal:
No subgoals!


Goal 3
==

  [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ (x1, x2) ⟹ v ≠ x1
  [1]Applying instance of rewrite rule ??.unknown:
?a1 ♯ ?x1.1 ⟹ ?a1 ♯ ?x2.1 ⟹ ?a1 ♯ (?x1.1, ?x2.1) ≡ True
  [1]Trying to rewrite:
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
  [2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
atom v ♯ x1
  [2]Applying instance of rewrite rule Nominal2_Base.fresh_at_base_2:
?a1 ♯ ?b1 ≡ ?a1 ≠ atom ?b1
  [2]Rewriting:
atom v ♯ x1 ≡ atom v ≠ atom x1
  [2]Applying instance of rewrite rule 
Nominal2_Base.at_base_class.atom_eq_iff:
atom ?a1 = atom ?b1 ≡ ?a1 = ?b1
  [2]Rewriting:
atom v = atom x1 ≡ v = x1
  [1]FAILED
atom v ♯ x1 ⟹ atom v ♯ t ⟹ atom v ♯ (x1, x2) ≡ True
  [1]Adding rewrite rule ??.unknown:
atom v ♯ x1 ≡ True
  [1]Adding rewrite rule ??.unknown:
atom v ♯ t ≡ True
  empty result sequence -- proof command failed

___
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

Re: [isabelle-dev] simplifier trace (and jedit)

[Thomas Sewell]

The _2 v.s. (2) thing is just silly. It's in find_theorems output too. 
It's just the way theorems get their names - probably one of these 
decisions made years ago and not compatible with Makarius' decisions 
about how to fetch theorems in Isar.


Adding context information to every reduction sounds too big in most 
cases - both for human consumption and for processing by fragile 
processes like ProofGeneral. I agree with you though that context can be 
hard to follow.


As for (simp only: ) vs unfolding - your rule is of the form Not (Suc 
nat = 0) which the simplifier preprocesses into (Suc nat = 0) == 
False but which the naive unfolder processes as (Not (Suc nat = 0)) == 
True. That is, without further setup, the rule is not really an 
unfoldable rule.


Yours,
Thomas.

On 23/05/12 14:15, Christian Sternagel wrote:

Dear all,

I wanted to write this already a long time ago (prompted by an Isabelle
course I gave) but somehow forgot about it. Now I had a look at my
slides again and was reminded.

1) The first thing is rather subjective, but maybe you could comment on
it. I think the simplifier trace would be less surprising for newbies
and slightly easier to read if
- names of rewrite rules would be printed in their original form.
Consider, e.g., the trace resulting from

lemma Suc 0 + 0 = 0
  using [[simp_trace]]
  apply simp

where we have (among others)

[1]Applying instance of rewrite rule Nat.nat.distinct_2:
Suc ?nat'2 = 0 ≡ False

Why not use the real name Nat.nat.distinct(2) in the trace (Okay,
the rule was preprocessed by the simplifier, but still, as far as I
can tell the printed name does not exist)?

- in the [1]Rewriting: messages, we actually just see the redex and
the contractum, but not the context of a rewrite step. Why not show the
whole terms? (One reason against this is the high redundancy and
potentially huge size of such traces, but on the other hand, they are
traces and only generated when requested.)

2) Some questions concerning the trace:
- When I explicitly use a single rule by unfolding rule-name, why is
there more in the trace than just the application of this rule?

- Why does apply (simp only: rule) and unfolding rule behave
differently? E.g., on the term Suc 0 = 0 with rule
Nat.nat.distinct(2) the former results in False, whereas the latter
does nothing. Is it important that those two commands behave differently?

3) Furthermore, in my course I recommend students (which know about term
rewriting before) to have a look at the simplifier trace whenever the
simplifier does something unexpected or does not terminate. However, for
the latter use-case (i.e., finding cause of nontermination) I do not
even know how to do it myself in jedit. As soon as I write, e.g., apply
simp the simplifier starts to loop, if I don't delete the command it
continues looping (and thus the whole system becomes highly unresponsive
very soon), if I delete the command, the trace is gone too. Is there any
way (or workaround), such that I can generate (part of) the trace of a
(potentially) looping reduction. Maybe giving a timeout to apply simp
(but I don't know whether or how this is possible) does work?

cheers

chris
___
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] record: fold_congs/unfold_congs

[Thomas Sewell]

The fold_congs theorems are not an accident. They are used as congruence 
rules to perform conversions such as
rec (| x := rec x + 1 |) = x_update (%x. x + 1) rec. Note this removes 
the duplicated mention of the name rec.


The name fold_congs is somewhat arbitrary, since either direction above 
could be argued to be folding.


This is used in our modified version of the Schirmer Hoare VCG. I 
suppose that we've released the c-parser sources (which load extra 
fold_congs) but not the modified Hoare package (which uses them). The 
point is to avoid an exponential time/space explosion when updates of 
the form % rec. rec (| x := rec x + 1 |) are performed in sequence. 
(The problem is the repeated rec.)


The fold_congs can be provided manually to the simplifier if anyone 
knows to do so. I am probably the only person in the world who knows 
when to do so. This is usually done to equate the two forms given above, 
either of which may be the result of other simplification. There are 88 
uses of fold_congs in the L4.verified proofs at this time.


The unfold_congs are meant to perform the reverse substitution, but the 
simplifier doesn't reliably play along. There are 5 uses in the 
L4.verified proofs at this time, and I suspect they can be easily removed.


Yours,
Thomas.

On 18/04/12 00:37, Makarius wrote:

This is probably mainly relevant to NICTA users of the record package.

When doing some cleanup and performance tuning of the record package, I
discovered the following mysterious fold_congs and unfold_congs:
http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334

They appear to go back to the initial NICTA contribution 50406c4951d9. I
have also seen traces of that feature in the L4.verified C parser tool
that became publicly available recently.

Do these fold_congs/unfold_congs still have any purpose?  In the reachable
set of Isabelle and AFP applications they don't, as far as I can see.  So
it looks like a candidate for garbage collection on the sources.


Makarius
___
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] Towards the next release

[Thomas Sewell]

We have a somewhat useful tool for expanding word equalities/inequalities 
bitwise, based on a part of some work Sascha and I did back in 2010. I've been 
meaning to push it up to the distribution for years, this will probably be a 
good time.

The main reason I'm telling you this is that I'm now more likely to actually do 
it.

Yours,
Thomas.

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] More context on Isabelle memory consumption

[Thomas Sewell]

My email about PolyML and memory usage has generated some discussion, 
perhaps I

should give some more context.

The L4.verified project has been stuck at Isabelle-2009-2 for years. Our 
proofs

seem to be compatible with newer Isabelle versions, but we're running out of
(virtual) memory. We've been running PolyML in 32 bit mode on most of our
machines. As images grow beyond 4GB, we must switch to 64 bit mode, which
roughly doubles memory use to  8GB, which means replacing most of our 
laptops.

Soon 16GB will be standard, I suppose.

In the meanwhile I've been having a look at Isabelle memory use. I've never
really understood why Isabelle images consume gigabytes of memory. With full
proofs off, the only real inputs should be the statements of hypotheses 
and the
definitions of types and terms. Isabelle's output is many orders of 
magnitude

bigger than these inputs.

The initial thought was that the record package would be representative. The
HOL image has grown because it has more in it, but the theorems generated in
defining a large record stay roughly constant. In addition, the L4.verified
proofs require a large record.  I attach a graph of the memory cost of 
defining

a 400-element record at various dates in Isabelle's development history. To
quote a Dilbert-like comic I read This graph clearly demonstrates up-ness.
The cost of defining the record has nearly tripled in this time.

We've had a look at some of the bigger spikes in this graph, and learned 
very

little of use. What is clear is that nothing is constant: the record package
has been moved from the Typecopy package to the Typedef package, which 
itself

has been growing in complexity, and throughout this time Florian has been
adding new hidden constants to the record package for code generation and
quickcheck. The record package uses multiple typedefs to simplify the 
types of
some terms. In 2009-2 a typedef caused a theory to be checkpointed 8 
times, in

2011-2 30 times.

This gives us a large collection of hypotheses, all of which are tedious to
investigate. Please appreciate how valuable empirical data from PolyML 
is. Up

until now we've been poking at these issues in the dark.

One point of reference is that disabling the code generation and random
extensions saves us about 30% memory consumption, (roughly doubling over
2009-2 rather than tripling) which may be a sufficient stop-gap measure.

To address Andreas' concern: this is memory usage *after* finishing a theory
and garbage collection. If you're writing tactics, don't worry about it too
much. We don't have a problem with individual proofs exhauting memory and we
aren't using full proofs. I anticipate anyone using full proofs will do 
so on a

machine with lots of memory.

Term sharing might be important for terms that are expected to end up at 
global

scope, e.g. statements of theorems or terms stored in various kinds of Table
for internal use. In addition, it will only matter if these terms are really
big or produced very often. The last line in the HOL statistics line was 13
million words worth of type substitutions. I guess the interesting 
question is

what terms are so large or being substituted so often.

The reason I'm sending these emails rather than proposing a patch is 
that I've
got lost trying to figure out which functions matter and which don't. I 
still

don't have any clear ideas.

Yours,
Thomas.

p.s. I attach the source of the graph as well. The columns are patch 
date, patch ID (hg name) and heap size in bytes. The date here is given 
in UNIX time for obscure reasons, gnuplot can read it with timefmt '%s'.


1282234761 004c35739d75  1342966296
1286379486 03174b2d075c  1330457808
1272362827 05209b869a6b  675239544
1269797642 095b1022e2ae  674991120
1286200717 0b8e19f588a4  1345002528
1271923982 0e24322474a4  806056288
1282722294 0e2596019119  1571638920
1285941925 10097e0a9dbd  1330533320
1283528624 12f3788be67b  134298
1286273097 132b79985660  1330457808
1283769525 14b16b380ca1  1571891264
1282806720 14c1085dec02  1425028072
1286267450 186a3b447e0b  1573254616
1278073397 19e8b730ddeb  1083742016
1284468473 1c4e38d635e1  1425157096
1269876649 1cd962a0b1a6  675207160
1277803530 1e99d8fc3d07  1326509472
1284300363 1f8131a7bcb9  1572107824
1282675008 20d82e98bcd7  1287225584
1282673370 20ff5600bd15  1569698432
1271862386 25e69e93954d  675437416
1269722068 26e820d27e0a  674980176
1289297835 27c1a1c82eba  1573443056
1284370555 27fae73fe769  1425167920
1285945609 2ffe7060ca75  1330538584
1286267291 317010af8972  1573254616
1288344928 323f7aad54b0  1573149976
1275474522 32b3d16b04f6  1266729032
1275383931 32c5251f78cd  675426536
1276866201 3489cea0e0e9  1326002400
1273626418 34dc65df7014  675258432
1275324572 3625d37a0079  675426536
1269711791 380b97496734  675066320
1282653389 38a926e033ad  1287225584
1278024058 40424fc83cc1  1073960320
1278084464 411717732710  1083742016
1284317267 44e4d8dfd6bf  1336187208
1282593352 458d6b12  1287225584
1290609215 

[isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

[Thomas Sewell]

Good day all. Just wanted to let the Isabelle developers know about the latest 
feature David Matthews has added to PolyML, and to let you all know how useful 
it is.

The feature allows profiling of objects after garbage collection. When code is 
compiled with PolyML.compiler.allocationProfiling set to 1, all objects 
allocated are also given a pointer to their allocating function. When the 
garbage collector runs with PolyML.compiler.profiling set to 4, a statistical 
trace is printed of which objects survived garbage collection.

This means that for Isabelle we get our first real look at what is taking up 
space at runtime and in images.

I include the last 20 lines of traces produced at four interesting points
  1) After including the HOL theories in HOL's ROOT.ML
  2) After performing a PolyML.shareCommonData after (1)
  3) After adding a 400-element record to a test theory built on the HOL image.
  4) After performing a shareCommonData after (3)

The output is currently a bit raw, since I'm not sure what the units are
(bytes? words? objects?). I suspect objects, since the total is roughly a tenth
of the runtime size. The other difficulty in interpreting this is the function
call graph. Small functions inlined into others are counted as their parent.
Library functions called from many places are counted against all of them
simultaneously.

Things for Isabelle developers to note from this:

Isabelle is generating a *lot* of copies of types  terms, particularly via
Term.map_atyps. Since shareCommonData eliminates them, many are
duplicates. It's possible that further use of the same variants from
Term_Subst might help. It's also possible that the repeated reconstruction is
necessary (e.g. repeated generalization/abstraction of type variables) and
further use of the new Term_Sharing mechanism might be the answer.

A large quantity of the persistent objects are Table and Net objects, as
expected.

There are surprisingly many dummy tasks.

A surprisingly large quantity of the persistent objects are associated with
proof terms and name derivations. This is presumably not Thm.name_derivation
but inlined code from its subcalls Proofterm.thm_proof, proof_combP,
proof_combt' and Library.foldl, none of which are listed. If indeed these foldl
loops are producing this many objects then perhaps the work done unconditionally
here should be rethought.

Traces:

1) After including the HOL theories in HOL's ROOT.ML

824925 Term_Subst.instT_same(3)subst_typs(1)
918632 Task_Queue.dummy_task(1)
942473 Net.insert(4)ins1(2)
   1032196 Term.map_atyps(2)
   1046107 Term_Subst.inst_same(4)subst(1)
   1058304 Term_Sharing.init(2)typ(1)
   1172790 List.map(2)
   1194308 Term.map_atyps(2)
   1356790 List.map(2)
   1377084 Table().modify(3)modfy(1)
   1875680 Term_Sharing.init(2)term(1)
   2688712 Type.strip_sorts(1)
   3082276 Table().modify(3)modfy(1)
   3177593 Function code
   5746085 Strings
   5914517 Unidentified word data
   8216169 Term.map_types(1)map_aux(1)
   9206871 List.map(2)
   9424264 Table().modify(3)modfy(1)
  13085440 Term.map_atyps(2)

2) After performing a PolyML.shareCommonData after (1)

183492 Table().map_default(3)(1)
199062 List.map(2)
220528 Thm.transfer(2)
294270 Term_Subst.inst_same(4)subst(1)
350230 Thm.map_tags(1)(1)
461706 Ord_List.union(3)unio(2)
464109 Mutable data
478833 List.map(2)
562309 Term_Sharing.init(2)term(1)
581994 Proofterm.prepare_thm_proof(8)
674516 Thm.name_derivation(2)
700221 Net.insert(4)ins1(2)
918632 Task_Queue.dummy_task(1)
   1019993 Term.map_types(1)map_aux(1)
   1193305 Table().modify(3)modfy(1)
   2619583 Table().modify(3)modfy(1)
   2769346 Unidentified word data
   3177590 Function code
   4684257 Strings
   8033629 Table().modify(3)modfy(1)

3) After adding a 400-element record to a test theory built on the HOL image.

211270 List.map(2)
549768 Table().modify(3)modfy(1)
638246 Logic.varifyT_global_same(1)(1)
844780 Envir.norm_term2(2)norm(1)
972069 ListPair.map(3)
   1151428 Type.varify_global(3)thaw(1)
   1222416 List.map(2)
   1379140 Logic.varifyT_global_same(1)(1)
   1727520 Term.map_atyps(2)
   2397356 Type.strip_sorts(1)
   2675166 Thm.name_derivation(2)
   6035908 Term_Subst.map_atypsT_same(1)typ(1)
   6558968 Net.insert(4)ins1(2)
   7004076 List.map(2)
   8166615 Same.map(2)
  10044260 Logic.incr_indexes_same(2)incr(2)
  10359792 Term.map_atyps(2)
  14882581 Term.map_types(1)map_aux(1)
  15712284 List.map(2)
  23758208 Term.map_atyps(2)

4) After performing a shareCommonData after (3)

 19086 Ord_List.union(3)unio(2)
 20925 List.map(2)
 25107 Table().modify(3)modfy(1)
 30360 Thm.transfer(2)
 33459 List.map(2)
 49475 Term_Subst.inst_same(4)subst(1)
 54711 Term_Subst.map_types_same(1)term(1)
 55132 Table().modify(3)modfy(1)
 58414 Mutable data
 62876 Strings
 64358 Thm.map_tags(1)(1)
 72438 List.map(2)
 87924 

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Thomas Sewell]

I'm strongly in favour of an explicit set type.

I've been asked for advice by a number of novice Isabelle users and given the 
same recommendation: go make the development type-check under the old rules. 
Then the simplifier will start helping you rather than fighting you.

I suppose there might be an alternative strategy involving adapting the simpset 
or similar to try to standardise blended terms on set operations or function 
operations. But I don't think this is possible the way Isabelle works - if it 
were not the default noone then it would not help, and if it were then it would 
generate years of work in compatibility with the existing proof library.

Yours,
Thomas.

From: isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de 
[isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de] On Behalf Of Lawrence 
Paulson [l...@cam.ac.uk]
Sent: Thursday, August 11, 2011 11:09 PM
To: Florian Haftmann
Cc: DEV Isabelle Mailinglist
Subject: Re: [isabelle-dev] (Re-)introducing set as a type constructor  rather 
than as mere abbreviation

I hope that my position on this question is obvious. And if we decide to revert 
to the former setup, I would be happy to help track down and fix some problems 
in theories.
Larry

On 11 Aug 2011, at 13:43, Florian Haftmann wrote:

 Why (I think) the current state concerning sets is a bad idea:
 * There are two worlds (sets and predicates) which are logically the
 same but syntactically different.  Although the logic construction
 suggests that you can switch easily between both, in practice you can't

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

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Probable bug in let_simp simproc

[Thomas Sewell]

I spent a bit of yesterday trying to discover why the standard simpset 
was taking forever to simplify a large term I happen to have.


The term is folded down in such a manner that unfolding Let_def will 
cause it to grow extremely large, which turns out to be what is 
happening. Deleting the let_simp simproc from the simpset solves the 
problem.


The let_simp simproc is written in two halves. The first bit I can 
easily understand, and if I produce a simproc with just that code it 
does what is expected.


The second half is commented Norbert Schirmer's case, and is 
incomprehensible to me at the moment. Does anyone know, broadly, what it 
is meant to do? If I knew that I might be able to figure out what the 
problem was.


Yours,
Thomas.

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

[isabelle-dev] I'd like to better understand some operations from Local_Theory.

[Thomas Sewell]

Hello Isabelle developers.

I'm doing an experiment in which I need to programmatically construct a locale. 
For simplicity I used the same operations that Michael Norrish was using in the 
l4.verified C code parser, Local_Theory.define and Local_Theory.notes. This led 
to some strange behaviour.

Suppose I set up ML actions for adding a definition foo = True to a locale 
and for getting the constant named foo

locale test = assumes True
begin

ML {*
val add_foo = Local_Theory.define ((@{binding foo}, NoSyn), 
(Attrib.empty_binding, @{term True}))
  # snd;
fun get_foo ctxt = ProofContext.read_const ctxt false dummyT foo;
*}
ML {*
val ctxt = @{context};
*}

If I run the add_foo operation with local_setup, get_foo tells me foo is now 
the constant local.foo.

local_setup {* add_foo *}
ML {* get_foo @{context} *}

This looked promising for my experiment. However, performing these actions 
within a single ML block tells me foo is extracted by read_const as the free 
variable foo (with the correct type).

ML {* get_foo (add_foo ctxt) *}

That had me stumped for hours. It turns I can get the behaviour I want with 
judicious interspersing of Local_Theory.restore.

ML {* get_foo (Local_Theory.restore (add_foo ctxt)) *}

However I'm just reciting incantations at this point. Furthermore I had no idea 
where to go looking for this incantation other than to try a collection of 
uncommented functions from Local_Theory. I've been a bit negligent about 
reading the various manuals that have cropped up of late; would any of them 
have explained what is going on?

Also, the behaviour if one supplies a functional pattern to local_setup has to 
be seen to be believed:

local_setup {* fn _ = add_foo ctxt *}
ML {* get_foo @{context} *}
ML {* get_foo ctxt *}

Although in writing this email I finally understood: the context saved in 
@{context} when ctxt was being defined includes the local ML interpreter state, 
which is one in which ctxt isn't defined yet. I guess that's what I get for 
playing with setup/local_setup.

I'll rephrase my question: should I have been better informed about this, or 
are local definitions genuinely inscrutable?

Yours,
Thomas.

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Feature request

[Thomas Sewell]

Hello Isabelle developers.

I was recently reminded of one of the things on my wish-list for Isabelle: a 
make -k mode in which the system continues for as long as possible and 
reports as many errors as possible, rather than halting after the first one. I 
think this would be generally useful to Isabelle users, but it would be 
especially useful when fiddling with tactics that are already in use. The usual 
approach is to try several variations aiming to minimise incompatibility, but 
there's no easy way to get an idea of the level of incompatibility without 
repairing the first few errors.

To clarify, I'd like to be able to type something like isabelle testmake 
(arguments), and the system would run through the same sources as on an 
isabelle make, only errors in proof scripts would be suppressed. Once 
everything is loaded and any image to be saved is saved, the system would print 
all the errors encountered at the end of the log.

It occurred to me how to implement this feature using the existing parallel 
apparatus. What's needed is a way to defer an exception raised in computing a 
future object forever, leaving the exception in the future and allowing all 
other independent work to conclude. Since parallel proofs are executed in 
future calculations that never need to be joined (unless someone is inspecting 
proof terms), this could provide a solution. I had a go at doing this myself 
but got nowhere. Does anyone familiar with the concurrency code think this is 
possible?

While I'm putting things on the concurrency wish-list, I have one more: a limit 
on the length of the work queue. The reason I request this is that some of our 
large sessions (1-2 hrs) seem to perform poorly with parallelism, and I suspect 
part of the problem is that the problem parsing thread is getting so far ahead 
of the problem-solving threads that the majority of the contexts and problems 
from the session are living in memory waiting to be solved. I think the way you 
would implement this is by switching mode once the work queue is large enough 
and dropping any threads attempting further forks to the bottom of the priority 
list. Does anybody else think this might be a good idea? I guess I should try 
to conjure up an example session which demonstrates the performance problems.

As always, please tell me if I'm completely wrong about the way the system 
works.

Yours,
Thomas.

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] FW: Safe approach to hypothesis substitution

[Thomas Sewell]

Let me try to explain the difference from the perspective of a user. There are 
three classical tools that will behave differently: safe, clarify and clarsimp. 
Each of these will, when it would have substituted and removed equalities in 
the past, now substitute those equalities, possibly reorient them, and leave 
them as hypotheses.

The additional equality will then be seen at all later points throughout tactic 
proofs. Given the ubiquity of clarsimp in my work, I suspect this changes the 
subgoal state at a significant number of points. The additional hypothesis will 
have little impact on most tools, but there are three kinds of tactic step with 
which it is a problem:
  1) Subgoals where a bound variable (typically 'x' or 'y') is renamed (to 'xa' 
or 'ya') because facts about x or y persist in the goal. This means that 
explicit instantiations in subgoal_tac etc may need to be updated.
  2) Explicit use of a drule or erule which can unify with an equality 
hypothesis (drule sym, drule_tac f=... in arg_cong, etc).
  3) Induction steps, where additional hypotheses complicate the induction 
hypothesis generated.

The changes to the HOL sources in the patch I sent reflect these three issues. 
None of these issues seem to be common, but maintainers of large repositories 
(HOL, the AFP, L4.verified etc) may still find them inconvenient.

The main advantage of the preserving an equality on a free variable is if that 
variable is reintroduced via facts from the context at a later point in the 
proof script. I think this is unlikely to occur in a terminal tactic (auto, 
blast, fastsimp, etc) and thus they are unlikely to benefit from the change. 
For this reason I added an unsafe wrapper which simulated the old behaviour. I 
haven't tested whether this was really necessary. I may do that tomorrow.

Yours,
Thomas.


From: Lawrence Paulson [l...@cam.ac.uk]
Sent: Tuesday, August 31, 2010 8:21 PM
To: Thomas Sewell
Cc: Isabelle Developers Mailing List
Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution

Thanks for looking into this problem, which has been around in one way or 
another from the very beginning.

Lost in all the technical discussions is the question of what the user will 
see. We have the option of leaving blast and force as they are now to minimise 
danger of incompatibility, though it would be disappointing if existing calls 
to these stopped working after what should be an improvement. I would expect 
them, on the contrary, to solve more problems than before. Anyway, the main 
methods to be affected are presumably safe and auto.

I have made a small table showing the number of times the classical proof 
methods are used in the HOL distribution:

safe956
auto23389
clarify 1403
force   1692
fastsimp 560
blast   7609
fast1079
best43

If the only method that behaves differently is safe, I wonder whether there's 
any point to doing this. It would be better to improve all the methods. If the 
new version is identical to the old one except that occasionally some 
equalities persist, then it ought to work as a drop-in replacement in nearly 
every instance. Is this what you see?

Larry

On 23 Aug 2010, at 08:52, Thomas Sewell wrote:

 As previously discussed in the thread Safe for boolean equality, the 
 current strategy for using equality hypotheses 'x = expr', in which 
 substitution for x is done and then the hypothesis is discarded, is unsafe. 
 The conclusion of that discussion was that the problem was annoying but 
 fairly rare, that there is some concern it may become more common as local 
 are used more extensively, and that fixing it would probably require a 
 painful change to the behaviour of auto.

 The problem is that by forgetting what x equates to in our goal, we lose the 
 connection from the goal to the context outside our goal. There may be other 
 facts available that name x. There may also be schematic variables which 
 could be instantiated to hd x but not the bound variable replacing it.

 The simple solution in my mind is to keep the equality in the goal, and since 
 noone else seemed interested I thought I'd attempt to do this myself and see 
 how difficult it was. I attach the resulting patch. After several rounds of 
 bugfixes and compatibility improvements, it requires 23 lines of changes to 
 theories to rebuild HOL, HOL-ex and HOL-Word.

 The code change in Provers/hypsubst.ML adds code for counting the free and 
 bound variables in a goal, and checking whether either side of an equality 
 hypothesis is a unique variable, occuring nowhere else. The main substitution 
 algorithms avoid using such equalities and also preserve rather than delete 
 the hypothesis they select. There is a new tactic for discarding these 
 equalities, which is added as an unsafe wrapper in Context_Rules, allowing 
 all unsafe tactics to behave roughly as before. The version of hypsubst 
 called by blast is left unchanged

Re: [isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

Let's try to answer everyone again:

Alex:
I think I was wrong about the cases involving algebra. There may be something 
interesting going on. The prenormalisation phase calls clarify_tac, then 
full_atomize_tac, then some other stuff. With a Free variable x assumed to be 
even, the resulting goals with the old and new versions of hypsubst are of the 
form ALL k. P (2 * k) and ALL k. x = 2 * k -- P (2 * k). It's possible 
that the quantifier elimination process that follows doesn't know what to do 
with the additional implication, or maybe just its left hand side.

If the same problem occurs for more interesting examples, it could be fixed by 
following clarify_tac with Hypsubst.thin_triv_tac in groebner.ML.

Finally, the change to inspect_pair is indeed just a bugfix. I don't this check 
is needed for the simplifier driven version of hyp_subst anyway, so the bug 
shouldn't often be seen.

Makarius:
Indeed bounds, frees and consts can all be seen as the same kind of thing. At 
the moment the only real benefits of hyp_subst over asm_full_simp are 
robustness in the case of Vars and the capacity to reorient equations in order 
to rewrite bounds - frees - expressions. Adjusting this to rewrite bounds - 
frees - consts - expressions would be easy - is this what you are asking for? 
I don't see this as widely useful, but perhaps you have an application in mind.

Finally, the full run of isabelle make test is indeed quite broken, including 
apparently going into a loop while defining a record in Hoare_Parallel. I'll 
look into it.

Yours,
Thomas.

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

I'm pretty sure this one is a bug. Try typing this into your favourite 
Isabelle session:


lemma foo:
  fwrap f = (%v. f v) == P f
  apply clarify

And note the system hangs. I think this is a pretty good argument to 
support the case that it doesn't occur in any existing Isabelle scripts.


Just to be safe, though, I can test this change in isolation against all 
the HOL libraries and the AFP thisevening when my machine has spare CPU 
time. I guess I should test against Isabelle 2009-2 rather than a 
development snapshot since the AFP will be known to build?


Yours,
Thomas.

On 26/08/10 02:49, Makarius wrote:

On Wed, 25 Aug 2010, Thomas Sewell wrote:

   

Finally, the change to inspect_pair is indeed just a bugfix. I don't
this check is needed for the simplifier driven version of hyp_subst
anyway, so the bug shouldn't often be seen.
 

Often it is hard to tell what is a bug or an obscure feature required like
that by some other tool.

Anyway, I recommend to try that tiny bit of the change on all existing
Isabelle + AFP theories.  Then we can apply it independently, with a more
informative log message that fixed bug, though.


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


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

Re: [isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

It's interesting that my innocent thread on hypothesis substitution has been 
hijacked into a discussion about context-aware coding guidelines. I'm trying to 
steer clear of contexts - it would seem more elegant to me if there was a 
purely tactical solution to this problem.

To answer Andreas' question about blast_hyp_subst_tac:

I made some attempts, but it seemed that making blast_hyp_subst_tac share 
behaviour or even code with the other versions led to incompatibilities I 
didn't really understand. The patch I sent keeps blast_hyp_subst_tac strictly 
in compatibility mode with previous behaviour. I think you've outlined why 
there was a problem - blast is guessing incorrectly what the tactic will do. 
Perhaps in the future the Hypsubst ML structure could export its eq_var and 
triv_asm term inspection functions so blast would have a better idea what it 
would do (assuming blast can construct accurately what the subgoal passed would 
be).

To respond to Makarius' comment that the real trouble only starts when trying 
the main
portion of existing applications, and also doing some performance measurements 
...:

I've run the simplest performance measurement I can: rebuilding HOL and HOL-ex.

On my desktop machine at home:

Pre-patch: Finished HOL (0:11:32 elapsed time, 0:11:30 cpu time, factor 0.99)
With patch: Finished HOL (0:11:37 elapsed time, 0:11:33 cpu time, factor 0.99)

On my desktop machine at work:

Pre-patch:
Finished HOL (0:07:24 elapsed time, 0:07:22 cpu time, factor 0.99)
Finished HOL-ex (0:15:25 elapsed time, 0:15:21 cpu time, factor 0.99)
With patch:
Finished HOL (0:07:41 elapsed time, 0:07:41 cpu time, factor 1.00)
Finished HOL-ex (0:15:30 elapsed time, 0:15:23 cpu time, factor 0.99)

In both cases parallel features are off (ISABELLE_USEDIR_OPTIONS=-q 0 -M 1).

Obviously this is only the beginning of the story. As I mentioned before there 
are some obvious performance improvements that can be made to the tactic 
itself, which I avoided for the sake of clarity. Whether the additional 
assumptions are slowing down other tactics is hard to tell.

With regard to running a broader set of existing applications: I was hoping to 
get some agreement as to whether this is a desirable approach or not before 
investing much more time in repairing proof scripts. I've set the standard 
isabelle make -k test test running, which may produce interesting results but 
will more likely tell us that many proofs are broken in trivial ways.

Yours,
Thomas.

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

As previously discussed in the thread Safe for boolean equality, the 
current strategy for using equality hypotheses 'x = expr', in which 
substitution for x is done and then the hypothesis is discarded, is 
unsafe. The conclusion of that discussion was that the problem was 
annoying but fairly rare, that there is some concern it may become more 
common as local are used more extensively, and that fixing it would 
probably require a painful change to the behaviour of auto.


The problem is that by forgetting what x equates to in our goal, we lose 
the connection from the goal to the context outside our goal. There may 
be other facts available that name x. There may also be schematic 
variables which could be instantiated to hd x but not the bound 
variable replacing it.


The simple solution in my mind is to keep the equality in the goal, and 
since noone else seemed interested I thought I'd attempt to do this 
myself and see how difficult it was. I attach the resulting patch. After 
several rounds of bugfixes and compatibility improvements, it requires 
23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word.


The code change in Provers/hypsubst.ML adds code for counting the free 
and bound variables in a goal, and checking whether either side of an 
equality hypothesis is a unique variable, occuring nowhere else. The 
main substitution algorithms avoid using such equalities and also 
preserve rather than delete the hypothesis they select. There is a new 
tactic for discarding these equalities, which is added as an unsafe 
wrapper in Context_Rules, allowing all unsafe tactics to behave roughly 
as before. The version of hypsubst called by blast is left unchanged, as 
blast proofs seem to be highly sensitive to changes. There is plenty of 
room for optimisation, I tried to keep the diff readable.


Three kinds of proofs seem to need fixing:
  1. proofs where subgoal_tac or similar now needs to refer to xa 
rather than x.
  2. proofs where erule ssubst, drule sym/arg_cong/fun_cong etc need to 
be further specialised.
  3. proofs where variables are eliminated and then induction is 
performed, i.e. the word library. Explicitly adding apply 
hypsubst_thin seems the best solution.


At this stage I'm not sure how to proceed. I would be very happy to see 
safe get safer, but I'm not sure how acceptable this level of 
incompatibility is in an Isabelle change. There's an alternative 
approach I thought of recently but haven't tried yet - replacing used 
equalities with meta-equalities - which might reduce the 
incompatibilities of type 2.


I haven't checked whether there are any performance implications.

I'd be keen to hear what other Isabelle developers think.

Yours,
Thomas.


diff -r 2e1b6a8a0fdd src/HOL/Divides.thy
--- a/src/HOL/Divides.thy   Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Divides.thy   Mon Aug 23 17:33:59 2010 +1000
@@ -429,7 +429,7 @@
 apply (case_tac y = 0) apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac -(y * k) = y * - k)
- apply (erule ssubst)
+ apply (simp only:)
  apply (erule div_mult_self1_is_id)
 apply simp
 done
@@ -438,8 +438,7 @@
 apply (case_tac y = 0) apply simp
 apply (auto simp add: dvd_def)
 apply (subgoal_tac y * k = -y * -k)
- apply (erule ssubst)
- apply (rule div_mult_self1_is_id)
+ apply (erule ssubst, rule div_mult_self1_is_id)
  apply simp
 apply simp
 done
diff -r 2e1b6a8a0fdd src/HOL/HOL.thy
--- a/src/HOL/HOL.thy   Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/HOL.thy   Mon Aug 23 17:33:59 2010 +1000
@@ -871,6 +871,7 @@
   Hypsubst.hypsubst_setup
   (*prevent substitution on bool*)
   # Context_Rules.addSWrapper (fn tac = hyp_subst_tac' ORELSE' tac)
+  # Context_Rules.addWrapper (fn tac = Hypsubst.thin_triv_tac false ORELSE' 
tac)
 end
 *}
 
diff -r 2e1b6a8a0fdd src/HOL/Int.thy
--- a/src/HOL/Int.thy   Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Int.thy   Mon Aug 23 17:33:59 2010 +1000
@@ -542,7 +542,7 @@
 lemma negD: (x \Colon int)  0 \Longrightarrow \existsn. x = - (of_nat 
(Suc n))
 apply (cases x)
 apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x=y - Suc x in exI, arith)
+apply (rule_tac x=y - Suc xa in exI, arith)
 done
 
 
diff -r 2e1b6a8a0fdd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy  Wed Jul 28 06:38:17 2010 +1000
+++ b/src/HOL/Library/Multiset.thy  Mon Aug 23 17:33:59 2010 +1000
@@ -1116,7 +1116,7 @@
  apply (simp (no_asm))
  apply (rule_tac x = (K - {#a#}) + Ka in exI)
  apply (simp (no_asm_simp) add: add_assoc [symmetric])
- apply (drule_tac f = \lambdaM. M - {#a#} in arg_cong)
+ apply (drule_tac f = \lambdaM. M - {#a#} and x=?S + ?T in arg_cong)
  apply (simp add: diff_union_single_conv)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
@@ -1127,7 +1127,7 @@
  apply (rule conjI)
   apply (simp add: multiset_ext_iff split: nat_diff_split)
  apply (rule conjI)
-  apply (drule_tac f = \lambdaM. M - {#a#} in arg_cong, simp)
+  apply (drule_tac f 

Re: [isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

Hello again isabelle-dev.

I should clear up some confusion that may have been caused by my mail. I was 
trying to avoid repeating all that had been said on this issue, and it seems I 
left out some that hadn't been said as well.

This approach avoids ever deleting an equality on a Free variable during a 
'safe' reasoning step. It will substitute with that equality but keep it in 
place. This is a significant change to the intermediate state of some tactic 
scripts, thus the incompatibilities, especially on induction. It is somewhat 
surprising there aren't more such incompatibilities. There's no truly safe way 
to delete an equality on a Free variable without inspecting the whole context.

Since equalities are not deleted, care must be taken to avoid an infinite loop 
in which a substitution is repeatedly attempted. This is the reason for the 
uniqueness check - if x appears only in 'x = expr' then there is no more 
substitution to be done. Some subtleties were discovered experimentally:
  - 'x = y' should not be substituted if either x or y is unique, or else we 
enter a loop substituting x - y - x
  - 'expr = x' needs to be reoriented when it is substituted, or else hypsubst 
and simp will loop doing opposite substitutions.
  - 'x = y' is OK to substitute if y is a unique free and x is a non-unique 
Bound.

This is what is meant by a 'useful' substitution in the comment. Other 
equalities, which would cause a no-effect or cyclic substitution, are referred 
to as trivial (abbreviated triv) in this code. The language should probably be 
cleanup up to use a consistent set of names.

Let me address Alex's detailed comments:

1. In the HOL sources the algebra method is used to solve two problems about 
parity essentially by accident. No Groebner bases were involved, but the 
surrouding logic, which appeals to clarify_tac and a custom simpset, happened 
to solve the goal. With this change the simplified goal had an extra quantifier 
in it. Note that with this change terminal tactics operating in 'unsafe' mode - 
fast, best, etc - will call thin_triv_tac via Context_Rules and behave 
similarly to before. It is terminal tactics which take safe steps - like 
algebra - that are most likely to break.

2. Yes, count vars is a bit strange, as it will consider (%f. f) (%x. x) to 
contain two copies of Bound -1. The point is to count loose Bounds in the 
hypotheses as returned by Logic.strip_assums_hyp, which it gets right.

Yours,
Thomas.


From: Alexander Krauss [kra...@in.tum.de]
Sent: Monday, August 23, 2010 7:35 PM
To: Thomas Sewell
Cc: Isabelle Developers Mailing List
Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution

Hi Thomas,

Thanks for digging into this. The concrete patch is exactly what was
needed to advance this discussion. Here are a few comments. I am sure
others will have more...

 I attach the resulting patch. After
 several rounds of bugfixes and compatibility improvements, it requires
 23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word.

So it is painful (as there are a much more theories out there), but it
may work, and it may be worth the trouble in the long run.

 The code change in Provers/hypsubst.ML adds code for counting the free
 and bound variables in a goal, and checking whether either side of an
 equality hypothesis is a unique variable, occuring nowhere else. The
 main substitution algorithms avoid using such equalities and also
 preserve rather than delete the hypothesis they select.

Do I understand correctly that substituting the hypothesis is safe, but
discarding them afterwards is unsafe? Then, why should they not be used?

More importantly, why is it safe to use and discard an equality when the
variable occurs elsewhere in the goal? The equality itself could
interact with a fact from the context? Consider the contrived example

locale l =
   fixes x :: nat
   assumes neq: x ~= 0
begin

lemma x = 0 == x = x + 1 == False
apply safe

After safe, the lemma becomes unprovable, since the hypothesis that
contradicts the context is removed. It seems that your patch does not
fix this... (I haven't tried... just guessing from reading the code)


[...]

A few concrete remarks concerning the patch (which seems to be relative
to Isabelle2009-2):


 diff -r 2e1b6a8a0fdd src/HOL/Parity.thy
 --- a/src/HOL/Parity.thy  Wed Jul 28 06:38:17 2010 +1000
 +++ b/src/HOL/Parity.thy  Mon Aug 23 17:33:59 2010 +1000
 @@ -66,9 +66,10 @@
by presburger

  lemma even_times_anything: even (x::int) == even (x * y)
 -  by algebra
 +  by (simp add: int_even_iff_2_dvd)

 -lemma anything_times_even: even (y::int) == even (x * y) by algebra
 +lemma anything_times_even: even (y::int) == even (x * y)
 +  by (simp add: int_even_iff_2_dvd)

  lemma odd_times_odd: odd (x::int) == odd y == odd (x * y)
by (simp add: even_def zmod_zmult1_eq)

?!? Why is the behaviour of the algebra method changed?

 diff -r 2e1b6a8a0fdd src/Provers

[isabelle-dev] Beta/Eta normalisation and net matching.

[Thomas Sewell]

Hello Isabelle developers.

I was about to have another attempt at speeding up a tactic we implemented for 
L4.verified using net-matching. In reading Pure/net.ML I spotted the comment 
Requires operands to be beta-eta-normal. In rereading the existing 
biresolution_from_nets_tac code, however, I didn't spot any attempt to beta/eta 
normalise the terms passed.

It occurs to me that I don't even know whether theorems in Isabelle can be 
assumed to be beta/eta normal. Does anyone have any quick pointers on that? Is 
there a potential bug here? Don't go searching for it - I'm happy to build some 
test cases and search for the answer myself if noone knows.

Yours,
Thomas.

The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Method parsing, YXML and term construction.

[Thomas Sewell]

Hello to isabelle-dev.

Suppose some ML code I wrote has terms f, x and y. I'd like to be able 
to produce the function application f x y with the catch that f, x and 
y may all have type parameters that need to be adapted to each other. Is 
there any convenient facility for doing this in Isabelle at the 
term-manipulation level?

Specifically, f is a polymorphic constant, x is a simple function 
application generated by our ML code, and y is supplied by the user and 
must be parsed. So far, our code has simply generated the string 
expression f (x) (y) and passed it to Syntax.read_term. Using the 
parser to get around type problems seems the ugly way through, however.

In upgrading to Isabelle-2009 everything got broken, because the input 
for y may be wrapped in YXML code to annotate it with position 
information, which results in f (x) (y) causing a malformed YXML error 
(it's a forest, not a tree). Helpfully, isabelle strips the YXML 
annotations from the error message as it is printed, making it difficult 
to establish what the cause of the error is.

The simple workaround which I've implemented is to purge the YXML from y 
by passing it to YXML.parse and then flattening the XML tree down to 
only its Text elements. This gets the job done, but it seems like a good 
idea to look for an alternative approach. Assuming I instead construct f 
and x as terms in ML, and pass y to Syntax.read_term as intended, is 
there a helper API for specialising the resulting types so they apply to 
each other?

Yours,
Thomas.