Email Gateway (Oct 15 2022 at 15:24): 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
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:
the above (which of course can be amended, but it still is unnecessary
complexity)
people forgetting to check in generated web/ stuff, which causes the
publish script not to publish those files
cluttered history, especially for merges
Fabian
Last updated: Jan 04 2025 at 20:18 UTC