Re: [isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.
Dear all,
How about this?
ap2 f (x, y) = (f x, f y)
@{ap n} f (x1, ..., xn) = (f x1, ..., f xn)
@{ap n} sounds reasonable to me, however, due to the presence of apfst and
apsnd one might
think about adding an all to indicate that the function is applied to all
element. So what about
@{ap_all n}?
Cheers,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Problems with datatype-new
Dear all,
I have an unexpected problem when defining a datatype using datatype_new.
theory Test
imports
$AFP/Collections/ICF/impl/RBTSetImpl
begin
datatype_new ('a,'b) bar = Foo 'a 'b option 'b rs
(*
Proof failed.
1. ⋀g ga h.
local.bar.ctor_rec_bar
(λx. case local.bar.Rep_bar_pre_bar x of (l, la, xa) ⇒ h (g l)
(map_option (λx. x) la) xa) =
local.bar.ctor_rec_bar (λx. case local.bar.Rep_bar_pre_bar x of (x1, xa,
xb) ⇒ h (g x1) xa xb)
The error(s) above occurred for the goal statement⌂:
⋀g ga h. local.bar.rec_bar h ∘ local.bar.map_bar g = local.bar.rec_bar (λx. h
(g x))*)
end
The problem vanishes if I make the datatype slightly more easier, e.g., if
- I declare 'a or 'b as dead
- 'b option or 'b rs is changed to pure 'b
- 'a is dropped
Just wanting to report this,
René
Isabelle: 52dfde98be4a
AFP: 23c1c5591d9f
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] BNF, -: flag, and sizes
Dear all, I just wanted to report some unexpected behavior when adapting our theories to datatype_new. First of all, thanks for the development, the convenience of using this package is very welcome! (automatic generation of named selection, map, ..., speed, etc.). However, when playing around with -: I noticed that this changes the generated size-functions (and hence automatic termination proofs), although this change is not immediately visible. Consider the following theory. theory Test imports Main begin datatype'a list1 = Nil1 | Cons1 'a 'a list1 datatype_new'a list2 = Nil2 | Cons2 'a 'a list2 datatype_new (-:'a) list3 = Nil3 | Cons3 'a 'a list3 (* the sizes of all three list variants are identical *) thm list1.size(3-4) list2.size(3-4) list3.size(3-4) datatype 'a mix11 = Mix11 'a list1 list 'a mix11 | Nix11 datatype 'a mix12 = Mix12 'a list2 list 'a mix12 | Nix12 datatype 'a mix13 = Mix13 'a list3 list 'a mix13 | Nix13 (* the size of all three mix variants are identical *) thm mix11.size(3-4) mix12.size(3-4) mix13.size(3-4) datatype_new 'a mix21 = Mix21 'a list1 list 'a mix21 | Nix21 datatype_new 'a mix22 = Mix22 'a list2 list 'a mix22 | Nix22 datatype_new 'a mix23 = Mix23 'a list3 list 'a mix23 | Nix23 (* the size of mix22 is different from both mix21 and mix23. whereas size_mix21 != size_mix22 might be okay I would not have expected size_mix22 != size_mix23 i.e., toggling -: in list2/3 on and off has an impact on other size functions although there is no difference in the size functions for list2/3 *) thm mix21.size(3-4) mix22.size(3-4) mix23.size(3-4) (* we get the same behavior if we also use -: in mix *) datatype_new (-:'a) mix31 = Mix31 'a list1 list 'a mix31 | Nix31 datatype_new (-:'a) mix32 = Mix32 'a list2 list 'a mix32 | Nix32 datatype_new (-:'a) mix33 = Mix33 'a list3 list 'a mix33 | Nix33 thm mix31.size(3-4) mix32.size(3-4) mix33.size(3-4) end I'm referring to Isabelle d0e04fdf4276 Kinds regards, René -- René Thiemannmailto:rene.thiem...@uibk.ac.at Computational Logic Grouphttp://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Sciencephone: +43 512 507-6434 University of Innsbruck ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013
Dear David, There is definitely some continous bloat factor with every new release, although David Matthews was usually ahead of most big applications in recent years. In fact he is about to release Poly/ML 5.5.1 pretty soon, so a quick test with some repository version of Poly/ML might help (e.g. SVN 1843). I would suggest trying with the --stackspace option e.g. ML_OPTIONS='--stackspace 500' The Fail exception with Insufficient space arises in a number of places such as when trying to fork a thread. This requires memory outside the ML heap. The stackspace option keeps some space free from the ML heap for these purposes. I tried it, but the setting was not high enough: then even earlier sessions crash with a new 'Run out of store - interrupting threads' error message. This also happens if I set stackspace to 1500, but it succeeded with 5000. However, then still afterwards I get the usual poly(6820,0xb09a5000) malloc: *** mmap(size=16777216) failed (error code=12) *** error: can't allocate region error as before, if I use minheap=1000, or drop the minheap parameter. I would guess that this is when running the X86/32 version rather than X86/64. Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode. Here is my current setup: ISABELLE_BUILD_OPTIONS= ML_PLATFORM=x86-darwin ML_HOME=/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=--minheap 1000 --stackspace 5000 Best regards, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013
Dear David, I would guess that this is when running the X86/32 version rather than X86/64. Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode. Here is my current setup: ISABELLE_BUILD_OPTIONS= ML_PLATFORM=x86-darwin ML_HOME=/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin ML_SYSTEM=polyml-5.5.0 ML_OPTIONS=--minheap 1000 --stackspace 5000 You definitely don't want a value as large as 5000. I think the exception may be occurring with PolyML.shareCommonData. This needs memory outside the heap to hold some tables. If there is a lot of live data in the heap these tables can be large and if the heap is taking up most or all of the available virtual memory, a particular problem in 32-bit mode, you may get the above message and exception. Is that possible in this case? Most of the time, it indeed appears after the theories have been processed, and the heap-file is being generated. (e.g., I never get the error with isabelle build Check-DPP, only if I build the heapfile with isabelle build -b Check-DPP) Moreover, I now tested a bit the 64-bit version of poly, and there the error does not occur, even without specifying ML_OPTIONS. For me, this looks like the most sensible solution. It is safe to handle the exception and continue; it's just that the sharing process will not be complete so that the heap will be bigger than it might otherwise be. I see. Thanks for your helpful comments, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_10-Sep-2013
Dear all, first of all, thanks Makarius for taking care of the new release. Here are my first comments: After changing to Isabelle_10-Sep-2013, most of the theories could easily be adapted. However, I noticed that on my machines I often get an Insufficient memory error. Building Check-DPP ... poly(59646,0xacc9fa28) malloc: *** mmap(size=134217728) failed (error code=12) *** error: can't allocate region *** set a breakpoint in malloc_error_break to debug Fail Insufficient memory: /Users/rene/.isabelle/Isabelle_10-Sep-2013/heaps/polyml-5.5.0_x86-darwin/Check-DPP Check-DPP FAILED To be more precise, when using ML_OPTIONS=--minheap 1000 I did not get the error under Isabelle2013, but under Isabelle_10-Sep-2013, it often fails with setting. Fortunately, using ML_OPTIONS=--minheap 3000 mostly works, but it is still annoying, since with this setting, I cannot start two Isabelle sessions in parallel. Does someone else notice increased memory consumption / crashes? Here are the details of my machine: MacOS X 10.8.4, 2 x 2.8 Ghz Quad-Core Intel Xeon, 6 GB RAM I noticed a similar phenomenon on my laptop with the following setup: MacOS X 10.8.4, 2.2 Ghz Intel Core i7, 8 GB RAM Cheers, René IsaFoR: a2136da2b517 AFP: 5c7a1374860e ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Problems with Code-Generator
Dear all,
Chris and I have recently ported our libraries IsaFoR and TermFun to the
development version which worked nicely, except for one issue, which arises
when we want to import external proofs into Isabelle.
The below theory compiles in Isabelle 2013 without problems.
The problem is that no matter, how we adjust the imports / code_reflect
settings,
we get different errors with the repository version (6a7ee03902c3) when
invoking the apply eval statement in the last proof:
importing ~~/src/HOL/Library/Code_Target_Numeral, no code_reflect:
works, but not desired
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions nat,
but not int (as it worked in 2013):
Error: Type error in function application.
Function: Checker.checker : Checker.inta - Checker.proof - bool
Argument: (Int_of_integer (25 : IntInf.int)) : inta
Reason: Can't unify Checker.inta with inta (Different type constructors)
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions both
int and nat:
previous error disappears, but Abstraction violation: constant
Code_Target_Nat.Nat in last apply eval
importing ~~/src/HOL/Library/Code_Target_Numeral, code_reflect mentions only
int, but not nat:
same as before
trying to also load Code_Binary_Nat also did not help.
Any feedback is welcome.
Cheers,
René
theory Test_Import
imports Main
~~/src/HOL/Library/Code_Char
(* in repository: ~~/src/HOL/Library/Code_Target_Numeral *)
(* in 2013: *)
~~/src/HOL/Library/Code_Integer
~~/src/HOL/Library/Code_Natural
begin
definition parse_digit :: char = nat where
parse_digit c = (
if c = CHR ''0'' then 0 else
if c = CHR ''1'' then 1 else
if c = CHR ''2'' then 2 else
if c = CHR ''3'' then 3 else
if c = CHR ''4'' then 4 else
if c = CHR ''5'' then 5 else
if c = CHR ''6'' then 6 else
if c = CHR ''7'' then 7 else
if c = CHR ''8'' then 8 else 9)
datatype proof = N nat | I int
definition parse_proof :: string = proof where
parse_proof input = (case input of
t # d # _ =
if t = CHR ''n'' then N (parse_digit d)
else I (of_nat (parse_digit d)))
definition parse_proof_term :: string = Code_Evaluation.term where
parse_proof_term input == Code_Evaluation.term_of (parse_proof input)
ML {*
structure Parser =
struct
val parse = String.explode # @{code parse_proof_term}
end
*}
fun checker :: int = proof = bool where
checker n (N i) = (of_nat i * of_nat i = n)
| checker n (I i) = (i * i = n)
lemma checker_imp_square: checker n p ⟹ ? x. x * x = n
by (cases p, auto)
(* precompilation of checker-code, so that it does not need to
be recompiled on every invokation of eval later on,
strangely, in 2013 only nat must be registered as datatype, but not int *)
code_reflect Checker
datatypes (* in repo: int = _ and *) nat = _ and proof = _
functions checker Trueprop
declare checker_def[code del]
setup {*
let
fun import_proof_tac ctxt input i =
let
val thy = Proof_Context.theory_of ctxt
val prf = cterm_of thy (Parser.parse input)
in
rtac @{thm checker_imp_square} i
THEN PRIMITIVE (Drule.instantiate' [] [SOME prf])
end
in
Method.setup @{binding import_proof}
(Scan.lift Parse.string (fn input = fn ctxt = SIMPLE_METHOD'
(import_proof_tac ctxt input)))
instantiates a proof via ML, usually, the string would be some file
content
end
*}
lemma ? x :: int. x * x = 25
apply (import_proof i5)
apply eval
done
lemma ? x :: int. x * x = 25
apply (import_proof n5)
apply eval
(*
On repository version:
Abstraction violation:
constant Code_Target_Nat.Nat
*)
done
end
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problems with Code-Generator
Hi Andreas, Code_Target_Nat implements the type nat as an abstract type (code abstype) with constructor Code_Target_Nat.Nat, i.e., Code_Target_Nat.Nat must not appear in any equation of the code generator. Unfortunately, this declaration also sets up the term_of function for type nat to produce terms with this constructor. In the second example, your import_proof method uses the term_of function to get a term for the given proof (and the number contained in the proof) and introduces along with this number into the goal state. As term_of uses the forbidden constructor Code_Target_Nat.Nat, when you then apply eval, the code generator complains that the abstract constructor is part of the goal state. I now see the problem. The simplest solution is to introduce a new constructor for which you can prove a code equation. For example, the following defines a constructor Nat2 and redefines term_of for naturals to use Nat2. When you add it to your theory before declaring the parser structure, the second example works, too (tested with Isabelle 2b68f4109075). You then also have to reflect both nat and int as datatypes. I integrated this solution also in our larger development, and it works like a charm. Thanks! If nobody has a better solution, we should think of including this setup in Code_Target_Nat. At least from my side, I can confirm that the solution works nicely. Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP access confusion
Dear all, I recently got some message from sourceforge, that they changed their directory structure. So I have no problems accessing the afp at ssh://login@hg.code.sf.net/p/afp/code Perhaps you can try this, René Am 23.03.2013 um 11:01 schrieb Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: cf. doc/maintenance.html: Check out the archive from the mercurial repository with: hg clone ssh://login@afp.hg.sourceforge.net/hgroot/afp/afp afp-devel But hg pull ssh://fhaftm...@afp.hg.sourceforge.net/hgroot/afp/afp yields Remote: abort: There is no Mercurial repository here (.hg not found)! I'm stymied… Thanks for any hint, 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] Some missing setup for function package in combination with Option-type
Dear all, recently, I stumbled upon the problem, that there is no proper fundef-cong rule for map on Option-types. I added it manually to our developedment, but perhaps this should be integrated in Option.thy lemma option_map_cong[fundef_cong]: xs = ys \Longrightarrow \lbrakk\And x. ys = Some x \Longrightarrow f x = g x\rbrakk \Longrightarrow Option.map f xs = Option.map g ys by (cases ys, auto) Cheers, René ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Two simple beginners question
Dear all,
I'm currently trying to develop a package for automatic generation of linear
orders for datatypes.
I have already defined some functions which generate the corresponding
equations which encode the linear order.
Now the first question I have is how to store these functions:
- when registering the equations via the function package
(Function.add_function) I essentially have
a local theory transformer of type lthy - lthy
- afterwards, I would like to store the newly created constant of the function
symbol and some other data
in some global store so
that I can reuse it later in other generated orders. Here, I currently use
structure Ordering_Data = Theory_Data( type T = ...)
with the update function Ordering_Data.map (Symtab.update ...)
which is essentially a theory transformer of type thy - thy
- how is it now possible to combine these transformers into one method foo,
such that either
setup {* foo my_datatype *} or local_setup {* foo my_datatype *}
can both register the function via the function package, and also store all
informations in
the Ordering_Data store.
To be more precise: Is there a way to convert a function (lthy - lthy) into
a function (thy - thy)
or vice versa?
The second is a rather simple ML question:
- Is it possible to conveniently update single fields in a record as in OCaml?
E.g., val r1 = {a = 5, b = foo, c = ..} and many fields
val r2 = '' r1 where only b is changed to bar ''
(in OCaml: val r2 = {r1 with b = bar})
Best regards,
René
--
René Thiemannmailto:rene.thiem...@uibk.ac.at
Computational Logic Grouphttp://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Sciencephone: +43 512 507-6434
University of Innsbruck
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two simple beginners question
Am 02.12.2011 um 15:52 schrieb Lukas Bulwahn:
It is best practice to make your data storage local, i.e., to a Generic_Data
functor.
Then update the generic data storage with Local_Theory.declaration.
Looking in the sources for the usage of Local_Theory.declaration should give
you a rough pattern, how to employ this function.
The second is a rather simple ML question:
- Is it possible to conveniently update single fields in a record as in
OCaml?
E.g., val r1 = {a = 5, b = foo, c = ..} and many fields
val r2 = '' r1 where only b is changed to bar ''
(in OCaml: val r2 = {r1 with b = bar})
To my knowledge, there is no convenient update functions for record in ML
provided automatically.
Therefore, many developers just define the ones of interest with some
boiler-plate code.
thanks for the pointers, now I can continue.
Best regards,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
Thanks Alex, the fixed version works again for IsaFoR Am 20.09.2011 um 11:22 schrieb Alexander Krauss: partial_function(option) foo :: nat list \Rightarrow unit option where foo x = foo x works, but partial_function(option) foo :: 'a list \Rightarrow unit option where foo x = foo x yields the following error message. *** exception THM 0 raised (line 1175 of thm.ML): instantiate: type Alex seems to have fixed this issue with changeset 8b74cfea913a Yes, many thanks for reporting this one. It came in when I added the generation of induction rules (which is still somewhat unfinished) in df41a5762c3d. This also shows that partial_function isn't terribly well-tested at the moment. Alex -- René Thiemannmailto:rene.thiem...@uibk.ac.at Computational Logic Grouphttp://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Sciencephone: +43 512 507-6434 University of Innsbruck ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
Dear all, when using the September 2011 version, I spotted the following font problem under Mac OS Lion: record braces \lparr and \rparr are displayed as blanks (although the width is roughly half of a normal blank) I even emptied my .emacs file to see whether it was my specific setup that caused the error, but still the display error occurs. Cheers, René Am 18.09.2011 um 17:38 schrieb Makarius: After a few more rounds of fine tuning, my impression is that we are slowly converging. http://isabelle.in.tum.de/repos/isabelle/file/f80d918f8ac0/ANNOUNCE there is a tentative announcement based on current NEWS. Is there anything missing? Some of the collective tool and library changes may be emphasized further, if they can stand on their own as separate item. Are there any further things in the pipeline? In the final phase one needs a bit more organization than the push first, fix later cycle that occasionally happens outside this special season. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- René Thiemannmailto:rene.thiem...@uibk.ac.at Computational Logic Grouphttp://cl-informatik.uibk.ac.at/~thiemann/ Institute of Computer Sciencephone: +43 512 507-6434 University of Innsbruck ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
Dear all,
There are still some improvements to the Haskell serializer and the code
generator I would like to get into the release.
After some discussions with Florian, the remaining changesets are about ready
and final, so I can probably commit them till this Wednesday.
Afterwards, the code generator is probably best checked against the two
largest executable formalisations (JinjaThreads and CeTA) -- I will try to
get the developers to re-run these with a current repository version or the
first pre-release version.
When reading this post (and since we will port to the new distribution in any
way), I started to adapt our library to the upcoming version where I used the
bundle http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Sep-2011/download.html
After some first adaptations I got stuck when at the first place where we use
partial_function. It seems that the partial_function package is broken if
polymorphic types are used. (which was not the case in Isabelle2011)
partial_function(option) foo :: nat list \Rightarrow unit option where foo
x = foo x
works, but
partial_function(option) foo :: 'a list \Rightarrow unit option where foo
x = foo x
yields the following error message.
*** exception THM 0 raised (line 1175 of thm.ML): instantiate: type conflict
*** ?F :: (?'a2 list \Rightarrow unit option) \Rightarrow ?'a2 list
\Rightarrow unit option
*** \lambdafoo. foo :: ('a list \Rightarrow unit option) \Rightarrow 'a
list \Rightarrow unit option
*** At command partial_function (line 216 of
/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy)
or if I output sorts
*** exception THM 0 raised (line 1175 of thm.ML): instantiate: type conflict
*** ?F\Colon(?'a2\Colontype list \Rightarrow unit option) \Rightarrow
?'a2\Colontype list \Rightarrow unit option :: (?'a2\Colontype list
\Rightarrow unit option) \Rightarrow ?'a2\Colontype list \Rightarrow
unit option
*** \lambdafoo\Colon'a\Colontype list \Rightarrow unit option. foo ::
('a\Colontype list \Rightarrow unit option) \Rightarrow 'a\Colontype
list \Rightarrow unit option
*** At command partial_function (line 216 of
/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy)
I think this is a triviality since it looks to me that one just has to replace
?a2 by 'a,
but I do not know where to fix it.
After that, I'm happy to test any further version, also repository snapshots.
Cheers,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
