Email Gateway (Aug 22 2022 at 17:51): Email Gateway (Aug 22 2022 at 17:51):From: Lars Hupel <hupel@in.tum.de>
Dear list,
what is the usual workflow to test isolated changes to an AFP entry with
some dependents; notably, without having to build the entirety of the AFP?
There's of course the -B XYZ option, but that one doesn't include
sessions that session-import XYZ. Case in point:
$ isabelle-dev build -v -n -d '$AFP' -B Graph_Theory
...
Skipping HOL-Library ...
Skipping Graph_Theory ...
Skipping ShortestPath ...
Unfinished session(s): Graph_Theory, HOL-Library, ShortestPath
But it should also build Parity_Game:
chapter AFP
session Parity_Game (AFP) = HOL +
options [timeout = 600]
sessions
"HOL-Library"
Coinductive
Graph_Theory
theories
PositionalDeterminacy
AttractorInductive
Graph_TheoryCompatibility
document_files
"root.tex"
"root.bib"
Interestingly enough,
Session AFP/Parity_Game (AFP)
appears in the output of "-v", but it's not being built.
Is this intended behaviour?
Cheers
Lars
Email Gateway (Aug 22 2022 at 18:15):From: Makarius <makarius@sketis.net>
On 17/07/18 14:56, Lars Hupel wrote:
what is the usual workflow to test isolated changes to an AFP entry with
some dependents; notably, without having to build the entirety of the AFP?
This question is still not fully settled yet, despite newly emerged
options like isabelle build -B or -S.
My feeling is it should be also connected to Source Code Management
(Mercurial) and a public database of build results wrt. changeset
versions (e.g. via some HTTP server).
There's of course the -B XYZ option, but that one doesn't include
sessions that session-import XYZ. Case in point:$ isabelle-dev build -v -n -d '$AFP' -B Graph_Theory
...
Skipping HOL-Library ...
Skipping Graph_Theory ...
Skipping ShortestPath ...
Unfinished session(s): Graph_Theory, HOL-Library, ShortestPathBut it should also build Parity_Game:
Is this intended behaviour?
It was the intended behaviour when I introduced the option some months
ago, but I am now unsure about it. I have revisited that for the next
release candidate as follows:
https://isabelle.sketis.net/repos/isabelle-release/rev/c14a2cc9b5ef
changeset: 68706:c14a2cc9b5ef
tag: tip
user: wenzelm
date: Wed Aug 01 20:58:41 2018 +0200
files: NEWS src/Doc/System/Sessions.thy
src/Pure/Thy/sessions.scala src/Pure/Tools/build.scala
description:
isabelle build options -c -x -B refer to imports_graph;
Considerable complexity has accumulated in isabelle build options, and
some combinations might still lead to surprises. Hopefully this is
sufficient for a reasonable simple and stable state for the release.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC