[isabelle-dev] export_code theory wildcard exports too much
Hi, I'm currently trying to "mitigate" the changes to export_code, which only inserts needed constants into the signature. For one theory, I tried to use the wildcard "Theory._" -- but the then-generated code seems to include ALL exportable definitions of some point in time. For example, the generated code now includes the structures Quickcheck_Exhausting and Quickcheck_Narrowing, which seems rather odd. The documentation states "referring to all executable constants within a certain theory by giving name._", and I thought 'within' herer refers to 'defined in', opposed to 'available in'. > hg id 8fcbfce2a2a9 tip - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] transfer with integers needs including / not documented in NEWS
Hi, I'm currently porting my AFP-entry to the current Isabelle-dev (8fcbfce2a2a9). I noted that using transfer for integers now needs "including integer.lifting" to actually work, but I could figure this out only by observing similar changes made by Peter. I could not find any documentation on it in the NEWS file. Is there something I missed? Thanks, René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Cryptographic Signature ___ 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?
>> What is funny is that Proof General was actually one of the main >> reasons of moving only >> slowly in such token language reforms. > I am glad that PG still works for most of my theories and I try to keep > that state as long as feasible. There are already problems with new > keywords declared by AFP entries that are not listed in the keywords > file. 'isabelle keywords $SESSION' can be used to generate a new keywords file with all keywords of $SESSION. - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] >>> SCHEDULER: disposed 4 dead worker threads
Am 16.12.2013 16:52, schrieb Makarius: > On Sun, 15 Dec 2013, Christian Urban wrote: > >> My guess is that I notice this message already for at least a year. It >> is in fact so frequent that I assumed this is normal behaviour of >> Isabelle. > > So just one more thing on the long list of open problems that nobody > dared to report or cared about. > > The big problem of Isabelle2013-1 was a lack of serious testing towards > a truly stable release, but I misinterpreted the lack of problem reports > as absence of problems. Isabelle2013-2 is a bit better, but not really > there -- right *after* the release I've got again further observations > about certain oddities that were already there at the start of the RC > phase 8 weeks ago. Just a quick idea of mine: Could it be worthwhile to decouple the releases of the logic from the releases of the system-/user interaction? That is, have Isabelle--x and Isabelle/Tools--x.z with the invariant that for every z Isabelle--x and Isabelle/Tools--x.z work well together. Then changes like 'missing dialog in Isabelle/jEdit' and 'better termination of stray processes' are easier to push and are in another category than 'new datatype system'. Again: This is just a quick idea, and I have no insight into how feasible the differentiation is, especially on the very low levels. - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2013-2 release
If there will already be a new release, would it perhaps be possible to merge the fix (given there is a robust one) for this 'adhoc_overloading raises TYPE' issue [1] ? This error is quite puzzling. And it occurs even if one does not know what the packages 'adhoc_overloading' and 'coercions' are about; depending on theories using it (e.g. ICF) is sufficient. This is just meant as a plain question. I fully understand that this change might be seen as 'too large on this short notice'. Thanks, René [1] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-November/msg00146.html ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] New handling of int/nat
Am 11.09.2013 19:00, schrieb Florian Haftmann:
> Hi René,
>
>> in Isabelle2012 (and 2013?), the types "nat" and "int" where
>> (using Efficient_Nat) directly translated into SML's IntInf.int
>> on code_export.
>>
>> This does not happen anymore in Isabelle-dev -- here they are now
>> mapped to types in Arith.
>>
>> The new behavior yields problems when interfacing with the
>> exported code to other SML-code (type mismatch). What is the
>> proposed "new" way here? Port all definitions to use type
>> "integer" instead of "nat" ("natural" also maps to something in
>> Arith)? Or add a 'wrapper' to each definition?:
>
> there are official conversions between all those arithmetic types:
> int_of_integer, integer_of_int etc. These you can generate and
> rely on them in your interface code. So you are free to provide
> the interfaces either on the theory level or directly on the target
> language level.
>
Thanks. I've been a bit reluctant about using the Arith.* functions in
my handwritten SML-code (relying on generated stuff etc), hoping that
there was something automagical. But now where you've stated that it's
the way to go, I've done it like that.
- René
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289-17232
Office: MI 03.11.055
smime.p7s
Description: S/MIME Kryptografische Unterschrift
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] New handling of int/nat
Dear all,
in Isabelle2012 (and 2013?), the types "nat" and "int" where (using
Efficient_Nat) directly translated into SML's IntInf.int on code_export.
This does not happen anymore in Isabelle-dev -- here they are now mapped
to types in Arith.
The new behavior yields problems when interfacing with the exported code
to other SML-code (type mismatch). What is the proposed "new" way here?
Port all definitions to use type "integer" instead of "nat" ("natural"
also maps to something in Arith)? Or add a 'wrapper' to each definition?:
definition foo :: "nat => nat" where "foo x = x + 1"
definition foo_wrap :: "integer => integer"
where "foo_wrap x = x + 1"
lemma [code]:
"foo x = nat_of_integer (foo_wrap (integer_of_nat x))"
Or am I using the new theories in a wrong fashion / there is automation
I could use?
Thanks,
René
P.S.: Hopefully, this is the right mailinglist.
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289-17232
Office: MI 03.11.055
smime.p7s
Description: S/MIME Kryptografische Unterschrift
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mixfix-Syntax not recognized
Am 06.08.2013 16:41, schrieb René Neumann: > It is probably related to the thread "Subscripts within identifiers", > but I'm not definitly sure. Most definitly: This behavior has been introduced with rev 3ac2878764f9. The question that remains (I could not grok it from the other thread): Is it now completely forbidden to use superscripts (except for esup-bsup) for such cases? Or can one only use non-letters (like the aforementioned infinity)? - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055 smime.p7s Description: S/MIME Kryptografische Unterschrift ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Mixfix-Syntax not recognized
Am 06.08.2013 16:41, schrieb René Neumann:
> Hi,
>
> I'm currently on revision 8d8cb75ab20a, and mixfix-Syntax seems not
> recognized in all cases (it seems like the syntax is only recognized if
> the type is known, somewhat...).
>
> Toy-Example (⇧ = \<^sup>) :
>
> begin
> definition foo :: "'a list ⇒ nat" ("(_⇧ω)") where
> "foo xs = length xs"
>
> term "foo xs" -- "type nat (as expected)"
> term "xs⇧ω" -- "type 'a"
> term "(xs::'a list)⇧ω" -- "type nat (as expected)"
"xs ⇧ω" (note the space) works.
- René
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289-17232
Office: MI 03.11.055
smime.p7s
Description: S/MIME Kryptografische Unterschrift
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Mixfix-Syntax not recognized
Hi,
I'm currently on revision 8d8cb75ab20a, and mixfix-Syntax seems not
recognized in all cases (it seems like the syntax is only recognized if
the type is known, somewhat...).
Toy-Example (⇧ = \<^sup>) :
begin
definition foo :: "'a list ⇒ nat" ("(_⇧ω)") where
"foo xs = length xs"
term "foo xs" -- "type nat (as expected)"
term "xs⇧ω" -- "type 'a"
term "(xs::'a list)⇧ω" -- "type nat (as expected)"
lemma
fixes xs :: "'a list" -- "learning, I explicitly fixed xs"
shows "xs⇧ω = length xs" -- "but still does not recognize ω"
by (simp add: foo_def) -- "fails"
end
It works with Isabelle-2013, but already failed ~100 revisions ago in
-dev (unfortunately forgot to write the exact revision down).
It is probably related to the thread "Subscripts within identifiers",
but I'm not definitly sure.
Please just tell me, if I should test a couple more revisions
- René
--
René Neumann
Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München
Tel: +49-89-289-17232
Office: MI 03.11.055
smime.p7s
Description: S/MIME Kryptografische Unterschrift
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
