[isabelle-dev] Mira / AFP configuration problem?

[Lars Noschinski]

On 30.05.2013 19:21, Makarius wrote:
> We keep getting odd errors like this:
>
> Unknown option "parallel_proofs_reuse_timing"
>
> e.g. here:
>
> http://isabelle.in.tum.de/reports/Isabelle/report/715f292e5d3d4be1b9e1af4be0d136d0

Thanks for reporting.

> It seems to be some old AFP version that is tested here accidentally. I
> had parallel_proofs_reuse_timing at some point, but later discontinued it.

That is due to a typo in /home/isabelle-repository/repos/afp/hg/.hgrc. 
Whatever script is responsible for updating this repository (AFAIK, it 
is not mira) did apparantely not make any noise. Hence there were no 
updates since the 2013-05-05. Instead of

   [paths]
   default = http://hg.code.sf.net/p/afp/code

it had

   [fipaths]
   default = http://hg.code.sf.net/p/afp/code

I fixed this.

BTW: There are some uncommitted changes (to .hgignore) laying around in 
this repository. This looks very wrong to me.

BTW2: The checked out version there is very old (from 2010) -- should it 
be more current?

> What is also odd: ML_HOME="/home/polyml/polyml-svn/x86-linux"

This is also due to the old version of the AFP (the test configuration 
is in the repository).

Should be fixed. Please make noise if something still goes wrong.

   -- Lars