I would like to use some published theories from the AFP. After downloading and extracting the afp-current.tar.gz package, I tried importing them using
isabelle components -u /home/rsoeldner/repo/afp-2021-08-08/thys/ which fails with
*** Bad component directory: "/home/rsoeldner/repo/afp-2021-08-08". I'm using Isabelle
Isabelle2021: February 2021
I had a similar problem. Are you sure, the theorem files lie at
/home/rsoeldner/repo/afp-2021-08-08/thys/? I think I needed to rename the folder so that it matches the exact description on the website. But I don't know why...
Yes, should be the case :)
Did you try
isabelle components -u /home/rsoeldner/repo/afp-2021-08-08, ie without the
/thys at the end?
yes, same error.
With and without the trailing
isabelle components -u /home/kreuzer/afp worked for me, but if it doesn't for you, then I'm at the end of my wits.
Maybe have a look at https://isabelle.in.tum.de/dist/library/Doc/System/Misc.html, section Managing Isabelle components, if that can help you.
Anyone else has a suggestion?
Thank you Katharina
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-May/msg00055.html is related to your issue
Last updated: Feb 27 2024 at 08:17 UTC