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 /
?
Yes
Oh, ok. 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: Dec 07 2024 at 16:22 UTC