Stream: Mirror: Isabelle Development Mailing List

Topic: *** Failed to relativize href location

view this post on Zulip Email Gateway (Apr 22 2026 at 09:38):

From: Tobias Nipkow <nipkow@in.tum.de>

...
Presenting theory "Dyck_Language.Dyck_Language"
Presenting theory "Pure"
*** Failed to relativize href location
"/Users/nipkow/.isabelle/browser_info/HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html"
with wrt. base "/Users/nipkow/.isabelle/browser_info/AFP/Context_Free_Grammar"

AFP: parent: 16494:e2ca723aa27e tip
Isabelle: parent: 84518:f09a1737d3c0 tip

What am I doing wrong :)

Tobias

smime.p7s

view this post on Zulip Email Gateway (Apr 22 2026 at 09:57):

From: Makarius <makarius@sketis.net>

On 22/04/2026 11:37, Tobias Nipkow wrote:

...
Presenting theory "Dyck_Language.Dyck_Language"
Presenting theory "Pure"
*** Failed to relativize href location "/Users/nipkow/.isabelle/browser_info/
HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html" with wrt. base "/Users/
nipkow/.isabelle/browser_info/AFP/Context_Free_Grammar"

AFP: parent: 16494:e2ca723aa27e tip
Isabelle: parent: 84518:f09a1737d3c0 tip

What am I doing wrong :)

I've got something wrong in b8b99a2c5991 with the semantics of
File.relative_path vs. _.relativize(_) --- and need to investigate this further.

Makarius

view this post on Zulip Email Gateway (Apr 22 2026 at 11:03):

From: Makarius <makarius@sketis.net>

On 22/04/2026 11:57, Makarius wrote:

On 22/04/2026 11:37, Tobias Nipkow wrote:

...
Presenting theory "Dyck_Language.Dyck_Language"
Presenting theory "Pure"
*** Failed to relativize href location "/Users/nipkow/.isabelle/
browser_info/ HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html" with wrt.
base "/Users/ nipkow/.isabelle/browser_info/AFP/Context_Free_Grammar"

AFP: parent: 16494:e2ca723aa27e tip
Isabelle: parent: 84518:f09a1737d3c0 tip

What am I doing wrong :)

I've got something wrong in b8b99a2c5991 with the semantics of
File.relative_path vs. _.relativize(_) --- and need to investigate this further.

I would say it should work again with the subsequent change, but your "..."
above don't say in which situation the problem actually occurred, so I could
not reproduce it.

changeset: 84520:c50c2ebb9f7c
user: wenzelm
date: Wed Apr 22 12:45:30 2026 +0200
files: src/Pure/General/file.scala src/Pure/General/html.scala
description:
more permissive operation, for relative locations outside the base (amending
b8b99a2c5991, see also 02588021b581);

Makarius

Last updated: Apr 29 2026 at 06:25 UTC