[isabelle-dev] Odd branches on AFP

[Makarius]

Using "hg branches" on afp-devel produces this result:

default 6476:5000c34002cf
ltl 6474:53421953ad96


What is the purpose of branches in Mercurial repositories? I've never 
understood that feature.



Makarius

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

Re: [isabelle-dev] Isabelle/jEdit - Loading of AFP session images fails

[Makarius]

On Tue, 29 Mar 2016, Salomon Sickert wrote:

sickert$ bin/isabelle jedit -d "~/Documents/workspace/afp-devel/thys/" 
-l Automatic_Refinement

1:32:14 PM [Session.manager] [error] manager: *** Consumer thread failure: 
"Session.manager"
1:32:14 PM [Session.manager] [error] manager: *** Undefined session: 
“Automatic_Refinement"

The puzzling thing is, that Isabelle finds the session 
“Automatic_Refinement”, builds it and then complains that it doesn’t 
know what is. Any ideas on how to debug and fix this?


We have neither bugs nor fixes in Isabelle development -- these are two 
sides of the same coin -- ultimately leading into entropy and decay.



When there is a problem there are two possibilities:

(1) Someone who understands the relevant part of the system knows what 
needs to be done. This is the case here, see now c35012b86e6f.


(2) If nobody has concrete ideas, Mercurial allows to make empiric studies 
of the history via bisection.


The history is the "proof" for the state of the sources. This is why it is 
important to keep the history clean and easy to understand -- after 
months, years, decades.



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

[isabelle-dev] Isabelle/jEdit - Loading of AFP session images fails

[Salomon Sickert]

Hello all,

I’m currently working with the current isabelle-devel (fe827c6fa8c5) and 
afp-devel (6143a36 
)
 and I have issues loading session images built from the AFP. For example 
loading HOL-Library works fine:

> sickert$ bin/isabelle jedit -d "~/Documents/workspace/afp-devel/thys/" -l 
> HOL-Library

However, if I want to load a session from the AFP:

> sickert$ bin/isabelle jedit -d "~/Documents/workspace/afp-devel/thys/" -l 
> Automatic_Refinement
1:32:14 PM [Session.manager] [error] manager: *** Consumer thread failure: 
"Session.manager"
1:32:14 PM [Session.manager] [error] manager: *** Undefined session: 
“Automatic_Refinement"

The puzzling thing is, that Isabelle finds the session “Automatic_Refinement”, 
builds it and then complains that it doesn’t know what is. 
Any ideas on how to debug and fix this?

Thank you,
Salomon___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev