Email Gateway (Aug 22 2022 at 19:07): Email Gateway (Aug 22 2022 at 19:07):From: Lars Hupel <hupel@in.tum.de>
Dear José,
I downloaded this library and copied in "~~/src/HOL/Algebraic_Numbers/".
there are two problems with this approach.
1) The single-entry downloads have become mostly useless now that many
AFP entries depend on others. Don't use them, just download the entire AFP.
2) Unless you're planning to change Isabelle's library, you shouldn't be
adding content to "$ISABELLE_HOME". This might create problems further
down the line (e.g. it becomes non-obvious what your actual dependencies
are). Put the AFP somewhere in your "$HOME".
Cheers
Lars
Email Gateway (Aug 22 2022 at 19:08):From: Lars Hupel <hupel@in.tum.de>
Hi José,
5) I wrote in the terminal: echo "/home/myself/afp/thys" >>> ~/.isabelle/Isabelle2018/ROOTS> Remark: I forget to substitute
"myself" by my actual name "> josemanuelrodriguezcaballero"
why don't you change that entry in the "ROOTS" file, then?
Cheers
Lars
Last updated: Apr 20 2024 at 04:19 UTC