Re: [isabelle-dev] build -x not working anymore

2017-11-05 Thread Makarius 
On 03/11/17 18:43, Fabio Madge Pimentel wrote:
> Building all of Isabelle including the AFP doesn’t work anymore. This can be 
> reproduced with the latest development versions, as well as the tagged 
> Isabelle2017 versions.
> 
>   ./isabelle build -ad ~/afp-devel/thys/ -x HOL
> 

For clarity a problem report should always include some error output.
For Isabelle2017 and the above invocation that is:

*** isabelle.Graph$Undefined

The option -d ~/afp-devel/thys/ is actually irrelevant here. The problem
is about unusual situations of option -x and -X.


I have now produced the following change
http://isabelle.in.tum.de/repos/isabelle/rev/671decd2e627 :

changeset:   67012:671decd2e627
tag: tip
user:wenzelm
date:Sun Nov 05 16:57:03 2017 +0100
files:   src/Pure/General/graph.scala src/Pure/Thy/sessions.scala
description:
uniform graph restriction: build_graph is more sparse than imports_graph
and may yield different results for exclude_session_groups /
exclude_sessions (e.g. "isabelle build -a -X main");


Makarius



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] build -x not working anymore

2017-11-03 Thread Makarius 
On 03/11/17 18:43, Fabio Madge Pimentel wrote:
> Building all of Isabelle including the AFP doesn’t work anymore. This can be 
> reproduced with the latest development versions, as well as the tagged 
> Isabelle2017 versions.
> 
>   ./isabelle build -ad ~/afp-devel/thys/ -x HOL

What is the purpose of option -x HOL here?

BTW, the normal place to discuss observations about Isabelle is the
isabelle-users mailing list.


Makarius




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

[isabelle-dev] build -x not working anymore

2017-11-03 Thread Fabio Madge Pimentel 
Building all of Isabelle including the AFP doesn’t work anymore. This can be 
reproduced with the latest development versions, as well as the tagged 
Isabelle2017 versions.

./isabelle build -ad ~/afp-devel/thys/ -x HOL

Fabio


signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev