Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Semantic hyperlinks: Hooray!


view this post on Zulip Email Gateway (Nov 10 2021 at 23:12):

From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
On 7/11/21 16:38, Makarius wrote:

Dear Isabelle users,

please see https://isabelle.sketis.net/website-Isabelle2021-1-RC2 and
https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1
for further progress on the release process.

The most notable change is HTML presentation with support for semantic hyperlinks!

This is great! Thank you very much for this update.

I've noted that the generated HTML has two kinds of links: one that
points to something like

#Theory.item|type

and the second kind points to

#offset_XXXX_YYYY

with XXXX and YYYY integers. The last kind seem to appear for items
declared inside a locale. Is this the reason of the difference?

view this post on Zulip Email Gateway (Nov 11 2021 at 07:59):

From: Fabian Huch <huch@in.tum.de>
Offset references are "internal" references that are not captured in the
foundational content. They should usually not be referred to from the
outside, and are not stable w.r.t. to changes in a theory.

This happens inside a locale, as locale parameters are treated as free
variables inside the context - but also, for instance, for named facts
inside a proof.

Fabian


Last updated: Jul 15 2022 at 23:21 UTC