Re: [isabelle-dev] Towards release
On 09/19/2011 01:56 PM, René Thiemann wrote:
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 \ unit option" where "foo x =
foo x"
works, but
partial_function(option) foo :: "'a list \ 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 \ unit option) \ ?'a2 list
\ unit option
*** \foo. foo :: ('a list \ unit option) \ 'a
list \ 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\(?'a2\type list \ unit option) \ ?'a2\type list
\ unit option :: (?'a2\type list \ unit option) \ ?'a2\type
list \ unit option
*** \foo\'a\type list \ unit option. foo :: ('a\type list
\ unit option) \ 'a\type list \ 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.
Alex seems to have fixed this issue with changeset 8b74cfea913a -- so,
if you can get hold on any version >= 8b74cfea913a, you can report if
there are further unresolved issues.
The mentioned changes of the code generator are also already in the
repository.
Lukas
Cheers,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
> 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. In my pocket is to move some theorems from Executable_Set.thy to more appropriate places, this should be done at the end of the week. Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] 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 \ unit option" where "foo
x = foo x"
works, but
partial_function(option) foo :: "'a list \ 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 \ unit option) \ ?'a2 list
\ unit option
*** \foo. foo :: ('a list \ unit option) \ 'a
list \ 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\(?'a2\type list \ unit option) \
?'a2\type list \ unit option :: (?'a2\type list
\ unit option) \ ?'a2\type list \
unit option
*** \foo\'a\type list \ unit option. foo ::
('a\type list \ unit option) \ 'a\type
list \ 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
Re: [isabelle-dev] Towards release
On 18.09.2011 17:38, Makarius wrote: 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. Two things from my side: - There is some tiny amount of reorganization left for Complete_Lattices (removing some "*_singleton" lemmas). Will probably push later this day; tests look good so far. - I'm working on integrating Haskabelle as a component. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
On Sun, 18 Sep 2011, Mamoun FILALI-AMINE wrote: Unofficial version of Isabelle/HOL (Isabelle repository snapshot 68615b48cc12 11-Sep-2011) The paths seem to be not set as before:when asking for a draft, pdflatex is not found (as before) Are you using Mac OS X? What does the following say in the Terminal? which pdflatex When using Macports it could be /opt/local/bin/pdflatex but MacTeX has /usr/textbin/pdflatex Note that for the Isabelle.app bundle the PATH is configured in Isabelle_11-Sep-2011.app/Contents/Resources/script Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
Hello all, 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. 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. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
On 18.09.2011 17:05, Makarius wrote: On Tue, 13 Sep 2011, Lars Noschinski wrote: I was irritated when Isabelle/jEdit complained about missing theory files, when the files where obviously there (and loaded). Later I found out, that this error is also displayed if there are any errors (transitively) in these theory files. Did you see the panel "Prover Session / Theory Status"? It provides some overview over the whole session. Yes, it's pretty useful. But at the I had above problem, it did not yet display the status in a way readable for the uninitiated ;) -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
