Karl Palmskog (Sep 09 2020 at 14:24): Karl Palmskog (Sep 09 2020 at 14:24):@Christian Doczkal I see that you created a gh-pages branch for comp-dec-modal. Are you sure you don't want to follow the usual structure from reglang and other coq-community repos, that are based on structuring the branch after tags and having a symlink to the latest tag documentation?
Karl Palmskog (Sep 09 2020 at 14:26):it's likely that we will automate this approach in the future, as described here: https://github.com/coq/bot/issues/85
Christian Doczkal (Sep 09 2020 at 14:41):Well, I pushed that branch before realizing that the templates provide no (easy) way to have documentation without tags and then I had other things to do. So no, I'm not sure that don't want to follow the usual structure ...
Christian Doczkal (Sep 09 2020 at 14:45):If I create a v1.0 release from the current master, would you be willing to take care of the rest?
Karl Palmskog (Sep 09 2020 at 14:48):@Christian Doczkal OK I can take care of it, but can I do a force-push on the gh-pages branch?
Christian Doczkal (Sep 09 2020 at 14:58):Sure, you can force push this, it's an accident after all. I have to go now, so I will do a release tomorrow and then ping you.
Christian Doczkal (Sep 10 2020 at 08:16):@Karl Palmskog I created a v1.0 release and I corrected the folder structure. What's the process for the index.html and the "coqdoc" badge. I'd actually prefer to do this myself so that I know the process.
Karl Palmskog (Sep 10 2020 at 08:19):@Christian Doczkal for index.html, I usually do two-step generation:
mustache meta.yml /path/to/index.md.mustache > index.md (adjust index.md manually here if necessary)pandoc -s -o index.html index.md Karl Palmskog (Sep 10 2020 at 08:19):for the badge, one just adds coqdoc: true in meta.yml and regenerates README.md
Christian Doczkal (Sep 10 2020 at 08:24):Argh, I just realized that I had two more commits (updated description and coqdocjs) on my machine that I hadn't pushed before tagging. :sad:
Karl Palmskog (Sep 10 2020 at 08:26):well, you can just remove the tag and tag again
Karl Palmskog (Sep 10 2020 at 08:26):at least better to discover this before it's in the opam repo.
Christian Doczkal (Sep 10 2020 at 08:44):Karl Palmskog said:
Christian Doczkal for index.html, I usually do two-step generation:
mustache meta.yml /path/to/index.md.mustache > index.md(adjustindex.mdmanually here if necessary)pandoc -s -o index.html index.md
Yes, that part is (kinda) obvious. But the coqdoc button on reglang links to the latest doc, while the button on the generated page links to the top-level page. Am I missing some meta info on the release, or do I need to manually fiddle with the README.md/index.html?
Karl Palmskog (Sep 10 2020 at 08:45):it used to give a direct link to toc.html in the templates, but someone did a PR to change it, and I haven't parameterized the link URL yet, so you will have to adjust it manually for now, yes
Karl Palmskog (Sep 10 2020 at 08:46):reglang is a good inspiration
Christian Doczkal (Sep 10 2020 at 09:03):Should be fine now, however I am slightly bothered by the fact that there is now a diff between the generated README.md and the checked in file. This means it's easy to accidentally erase the customization of the button when doing maintenance releases. The link target should probably be configurable via meta.yml.
Karl Palmskog (Sep 10 2020 at 09:06):I agree, and you are welcome to submit PRs to fix this. However, we have quite a few bigger problems right now, like the Nix CI on Cachix. Let's just say the manpower is not overwhelming.
Karl Palmskog (Sep 10 2020 at 09:16):the long term goal would be auto-submission and auto-merging of PRs for template updates in coq-community via the Coq bot. But I think we are quite far from that (a year?)
Karl Palmskog (Sep 11 2020 at 08:47):ah, have to also fix this part in the templates, the doc field in the opam package: https://github.com/coq-community/comp-dec-modal/blob/d54f5948f5dc2b7bb518bbc187ab5ba86f9720db/coq-comp-dec-modal.opam#L8
Karl Palmskog (Sep 11 2020 at 08:48):by default, it should probably point at the "latest" coqdoc, and then our automation should change this to a tag when submitting releases to the opam archive
Christian Doczkal (Sep 11 2020 at 09:57):@Karl Palmskog What's the purpose of these fields anyway? Is there any opam command (other than opam show) that uses them? But while we're on the topic, should the homepage really be the repository front page or should it rather be https://coq-community.org/comp-dec-modal/? I'm undecided/fine either way.
Karl Palmskog (Sep 11 2020 at 10:06):we make homepage the regular GitHub page currently, but it could be configurable. doc has some uses in opam, but we should try to follow what the OCaml community does with it I think
Karl Palmskog (Sep 11 2020 at 10:07):for example, if you want to reference documentation, you could use the doc field to pass a parameter to coqdoc
Karl Palmskog (Sep 12 2020 at 13:08):according to the opam manual, all of homepage, doc, and bug-reports are informal "URLs pointing to the related pages for the package, for user information". But of course, the Coq OPAM archive could use them in some more extensive capacity in the future.
Karl Palmskog (Sep 14 2020 at 11:29):@Christian Doczkal is the release of comp-dec-modal final now? I can submit an opam package to the archive if so.
Christian Doczkal (Sep 14 2020 at 11:38):@Karl Palmskog , yes, I'm not working on this for the moment. If I ever get around to replacing my old fset.v with finmap.v that will be a point release.
Karl Palmskog (Sep 15 2020 at 09:06):just curious, I might have missed this as I skimmed the papers, but why not include CTL* metatheory as well? Scope issue or due to technical reasons?
Christian Doczkal (Sep 15 2020 at 09:25):Well, the answer is relatively simple: I was mostly interested in proving completeness of inference systems and the inference systems for CTL* are ... messy. Even the "Hilbert-style" axiomatization includes arbitrary-width rules with complex syntactic side-conditions. So the proof theory of CTL* is an entirely different game. In fact, it might be more reasonable to attempt a formalization of the completeness proof for the µ-calculus, which has an extremely pleasing axiomatization (induction+fixpoint unfolding). However, the completeness proof requires very different techniques from those for the CTL/PDL familiy of logics, and is much longer (~40 pages rather than 4-5 per logic).
Last updated: Apr 17 2024 at 23:01 UTC