Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] isabelle build -B doesn't include all dependents


view this post on Zulip 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

view this post on Zulip 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, ShortestPath

But 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: Mar 28 2024 at 12:29 UTC