Search code examples
isabelle

How to skip (problematic) Isabelle sessions in AFP?

I tried to use AFP (02/22/2021) with Isabelle 2021, but the jEdit/Isabelle PIDE wouldn't load after the AFP directory is added to the user ROOT file. The is shown below and seems to be about a specific package:

enter image description here

I don't really need the entry in question (, or know what it does). My question is:

Is there a way to use a subset of AFPs and exclude problematic entries in the screenshot?

-- Update ---

As pointed out in the comments, the AFP seemed to be lagging a couple of days behind. Using afp-02-24-2021, the initial error went away. However, when selecting a session Jordan-Normal-Form from jEdit, there is a new error about JNF-AFP-Lib build failing, as shown below:

enter image description here

The question remains. The AFP seems to be a large collection and there could be multiple sources of error.

In case of such errors, is there a way to select a subset of AFPs to use or debug?

If not, is there a systematic way to test which afps do or do not build?

Solution

  • Original question

    The problem was because you (unknowingly) used an AFP release that did not match the Isabelle release. To avoid that problem in the future, I recommend using the Mercurial repository directly:

    https://foss.heptapod.net/isa-afp/afp-2021

    The Mercurial repository for a new Isabelle release gets created during the RC phase, so you can always be sure to have matching versions.

    In the case of these mismatches, it is usually not possible to select a subset of the AFP that "works", because between 2020 and 2021, the session management has changed considerably.

    Update

    The problem you're facing here is that you have selected a big session as a prerequisite and it takes too long to build with the default configuration.

    You can build the session on the command line with an increased timeout as follows:

    isabelle build -bv -d <path to afp>/thys -o timeout_scale=3 Jordan_Normal_Form

    Increase the factor if it keeps timeouting.

    General remark

    You ask, "In case of such errors, is there a way to select a subset of AFPs to use or debug?". The answer to that question depends on the kind of error. Your post currently contains two vastly different problems, so it's not possible to give a general answer, unfortunately.