Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] https://isabelle.in.tum.de/dist/library vs htt...

Email Gateway (Feb 18 2025 at 16:39):

From: Tobias Nipkow <nipkow@in.tum.de>
Both links seem to lead to the same files. Is one an alias for the other? Should
one be preferred over the other? The isabelle web pages use the dist variant.

Thanks
Tobias

smime.p7s

Email Gateway (Feb 21 2025 at 10:40):

From: Makarius <makarius@sketis.net>
On 18/02/2025 17:38, Tobias Nipkow wrote:

Both links seem to lead to the same files. Is one an alias for the other?
Should one be preferred over the other? The isabelle web pages use the dist
variant.

The Isabelle website and "dist" area has a couple of aliases, often for
unknown historic reasons. I can't say on the spot what is caninical: it would
require some research into the website build tool, and its not so glorious
history.

So the usual question: What is your application? Is it a permanent link in
some bibtex database? Or is it just an end-user who wants to browse the HTML
library?

In the latter case, Isabelle2025-RC3 now provides this (cf. NEWS):

"""
* Isabelle/jEdit Prover IDE *

• Action isabelle.browser_info or menu "Plugins / Isabelle / Browse HTML
  Library" opens a web browser on the HTML library that is distributed
  with Isabelle (if available, see $ISABELLE_HOME/lib/browser_info.db).
  """

Thus the browsed data is always the correct one, by construction of
Admin/build_release.

Makarius

Last updated: Mar 09 2025 at 12:28 UTC