I'm getting this message again. What gives? Everything is fully updated.
~/isabelle/Repos/src/HOL: hg id
2e5b737810a6 tip
Larry
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Category3.Limit" via "Category3.FreeCategory" via
"
> I'm getting this message again. What gives? Everything is fully updated.
>
> ~/isabelle/Repos/src/HOL: hg id
> 2e5b737810a6 tip
Do you have any uncommitted changes? Maybe in the AFP?
~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP'
works fine for me.
Cheers
Lars
_
It seems that I can fix this by updating afp-devel again.
Larry
> On 9 May 2018, at 12:37, Lars Hupel wrote:
>
> Do you have any uncommitted changes? Maybe in the AFP?
>
> ~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP'
>
> works fine for me.
_
On 26/03/18 13:48, Christian Sternagel wrote:
>
> Thanks, I forgot about that option.
>
> With "isabelle latex" in the specified directory the error boils down to:
>
> ./root.tex:31: Package pdftex.def Error: File
> `isabelle-eps-converted-to.pdf' n
> ot found.
>
> See the pdftex.def package do
On 10/03/18 11:06, Makarius wrote:
> On 08/03/18 13:08, Makarius wrote:
>>
>>> Since David Matthews has make a lot of changes concerning fine-points of
>>> heap management in the past few months, I would like to test it with
>>> some Poly/ML repository version. But this does not build on macOS at t