Re: [isabelle-dev] Bad session structure

2018-06-25 Thread Tobias Nipkow
This is because of a name change in the distribution. The AFP has been updated some 10 minutes later but your test run still saw the old version. It should work now. Tobias On 25/06/2018 15:25, Lawrence Paulson wrote: I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry

[isabelle-dev] Bad session structure

2018-06-25 Thread Lawrence Paulson
I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry Cannot load theory "HOL-Data_Structures.Priority_Queue" The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue" (required by "Priority_Queue_Braun.Priority_Queue_Braun") (line 7 of

Re: [isabelle-dev] bad session structure

2018-05-09 Thread Lawrence Paulson
It seems that I can fix this by updating afp-devel again. Larry > On 9 May 2018, at 12:37, Lars Hupel wrote: > > Do you have any uncommitted changes? Maybe in the AFP? > > ~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP' > > works fine for me.

Re: [isabelle-dev] bad session structure

2018-05-09 Thread Lars Hupel
> I'm getting this message again. What gives? Everything is fully updated. > > ~/isabelle/Repos/src/HOL: hg id > 2e5b737810a6 tip Do you have any uncommitted changes? Maybe in the AFP? ~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP' works fine for me. Cheers Lars

[isabelle-dev] bad session structure

2018-05-09 Thread Lawrence Paulson
I'm getting this message again. What gives? Everything is fully updated. ~/isabelle/Repos/src/HOL: hg id 2e5b737810a6 tip Larry Cannot load theory "HOL-Library.FuncSet" The error(s) above occurred for theory "HOL-Library.FuncSet" (required by "Category3.Limit" via "Category3.FreeCategory" via

Re: [isabelle-dev] Bad session structure: may cause problems with theory imports

2018-04-25 Thread Florian Haftmann
Hi Larry, I guess you have to update your local AFP clone also. Hope this helps, Florian Am 25.04.2018 um 18:03 schrieb Lawrence Paulson: > In the past couple of days, upon launching Isabelle jEdit, I get an alert box > with the message above and the attached text. Any ideas? > >

[isabelle-dev] Bad session structure: may cause problems with theory imports

2018-04-25 Thread Lawrence Paulson
In the past couple of days, upon launching Isabelle jEdit, I get an alert box with the message above and the attached text. Any ideas? Larry ~/isabelle/Repos/src/Pure: hg id 362baebe25a5 tip Cannot load theory "HOL-Library.Code_Char" The error(s) above occurred for theory