Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP entries with the new imports system

view this post on Zulip Email Gateway (Aug 22 2022 at 16:10):

From: Sebastien Gouezel <sebastien.gouezel@univ-nantes.fr>
AFP entries have been reformed to use the new imports system. For
instance, in my entry Lp, the line

imports "HOL-Analysis.Analysis" "../Ergodic_Theory/SG_Library_Complement"

has been replaced with

imports "HOL-Analysis.Analysis" Ergodic_Theory.SG_Library_Complement

and I understand this is the way to go. However, I did not find
documentation explaining how to setup Isabelle so that
Ergodic_Theory.SG_Library_Complement is correctly found on my computer
(it currently gives me Bad theory import
"Ergodic_Theory.SG_Library_Complement"). Is there a pointer to
up-to-date documentation regarding this? (for instance,
https://www.isa-afp.org/using.html is outdated in this respect)

Best,
Sebastien

view this post on Zulip Email Gateway (Aug 22 2022 at 16:12):

From: Lars Hupel <hupel@in.tum.de>
Dear Sebastien,

see
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-August/msg00053.html>
for the two choices you have.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 16:13):

From: Sebastien Gouezel <sebastien.gouezel@univ-nantes.fr>
Thanks, adding Ergodic_Theory to the ROOTS file works perfectly.

Sebastien

view this post on Zulip Email Gateway (Aug 22 2022 at 16:14):

From: Makarius <makarius@sketis.net>
There are some brief hints in the NEWS file: search for "imports" in the
section for Isabelle2017.

Moreover, the "system" manual has some general explanations as part of
the "isabelle imports" tool. See the diff here:
http://isabelle.in.tum.de/repos/isabelle/diff/41b64e53b6a1/src/Doc/System/Sessions.thy

Makarius

Last updated: Apr 20 2024 at 12:26 UTC