Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] AFP devel links redirect to stable


view this post on Zulip Email Gateway (Oct 15 2022 at 15:24):

From: Asta Halkjær From <andro.from@gmail.com>
Hi,

I just noticed that on the devel page for one of my entries:
https://devel.isa-afp.org/entries/FOL_Seq_Calc3.html

The list item "Syntax" contains this link:
https://devel.isa-afp.org/theories/fol_seq_calc3/#Syntax

It gets incorrectly resolved as a link to the stable AFP:
https://www.isa-afp.org/browser_info/current/AFP/FOL_Seq_Calc3/Syntax.html

It should instead be:
https://devel.isa-afp.org/browser_info/current/AFP/FOL_Seq_Calc3/Syntax.html

This does not seem unique to my entry.

Best,
Asta

view this post on Zulip Email Gateway (Oct 17 2022 at 08:44):

From: Fabian Huch <huch@in.tum.de>
[Cross-posting this to the afp-submit list where this discussion belong,
please don't answer to isabelle-users]

Yes that's a systematic problem (which has existed since the inception
of the AFP build system), since the AFP repository contains the built
website for the release version: On push to devel, the repository is
checked out (its web/ dir overwriting any devel pages), and only a
successful AFP build (which takes a few hours) will overwrite the web/
files again to the proper devel version.

The deeper question to the other editors: Is it really necessary to keep
everything checked in under web/? I don't really see an advantage, but
three routine problems:

Fabian


Last updated: Mar 28 2024 at 12:29 UTC