Inlined documentation

[strub]

No description provided.

[fdupress]

@MM45, can you please give a quick description of the syntax and intended usage, either in a PR or in a wiki page? This will help me review, given this should probably be a usage-based review.

[MM45]

Alright, so this most recent commit should fix all issues with external projects, but don't waste too much time on reviewing yet:

• We want to still (1) prevent any non-documentation comments that are put before a documented item from being included in the source, and (2) not fail on a misplaced documentation comment (but only warn instead). For these two things, it would be nice if you could help me by taking a quick look @strub: It is taking me quite some time figuring out how to best approach this in the parser.
• I will soon (TM) include an example "tutorial" file that explains all the functionality and what have you, which should both make reviewing this a lot easier, and it can immediately serve as (part of) the documentation.

[MM45]

@MM45, can you please give a quick description of the syntax and intended usage, either in a PR or in a wiki page? This will help me review, given this should probably be a usage-based review.

Well, that's a coincidence, I was just typing out my previous comment when you replied ^^ Anyways, I guess I should've changed this to a "draft PR", but I forgot. Sorry. See my previous comment. Only after fixing the things I mentioned there it should be reviewed (in my opinion), and I will ping here when that is the case.

[MM45]

Okay @fdupress, if the checks succeed, I think it should be reviewable: the resources/tests/EasyCrypt_DocGen_Tutorial.ec file should be all you need to get going. Note that the fixes of the issues I mentioned in my first comment here are not there yet, but these are sort-off QOL changes anyways. Let me know if anything is wrong or unclear.

[MM45]

Alright, now also the two QOL issues I mentioned before are dealt with (although there remains the warning from the parser that the new COMMENT token is not used. Do we care about this @strub?). Anyways, @fdupress, now it should really be reviewable, and I marked the PR as such^^

[fdupress]

Must absolutely fix the gendoc/docgen discrepancy. (Spotted once; stopped looking.)
Otherwise good to go if all comments are considered and reasonably dismissable.

[MM45]

Okidokie, I accidentally discovered a bug that made it such that documentation was generated for clones as if they were regular theories. Should be fixed now.

[strub]

@fdupress Is the PR ok for you?

[fdupress]

Yes, this is fine: Matthias has addressed my comments.

[MM45]

@strub I made an attempt at what we discussed: preventing docgen from checking any proofs. Not sure if this is the right approach though. Also, I added a check that prevents exiting if there is an eco file when doing docgen (I think this is desired behavior: probably you only generate docs after you check, in which case the eco file blocking docgen is annoying. However, we might consider a separate kind of eco for docgen at some point: it is not necessary to generate documentation anew when a file and its dependencies haven't changed)

[fdupress]

Regarding rebase: main has been merged in at regular intervals, so there is no change this will rebase cleanly on top of main without more time than I have now. We need to decide how to proceed. (Merge a spaghetti bowl, or put effort into rebasing.)

@strub, thoughts?

[strub]

Just squash the commits. Ask Matthias to write a proper commit message.

[fdupress]

Oh, excellent! Good thing I got distracted and did not work on it :)

[MM45]

Hmm, wait. Not sure what is going on, but seems to not be behaving as it used to before we started merging... For example, docgen now checks files and fails if the file doesn't check properly. Also, the warning about the unused COMMENT token is back... (This is even the case on a backup branch I made locally before squashing).

[fdupress]

Right. I'll try to checkout before the squash. Did you make sure to pull before squashing? (Could have forgotten some of the last commits otherwise.)

[MM45]

Yes, I did: pull, merge main into branch, diff main with branch, store diff in patch, reset branch to main, apply patch, commit, push. Just checked some of the final commits I did on this branch, particularly those that contained the logic concerning the (not) checking of proofs with docgen, and it all seems to actually still be there as far as I can tell. It just doesn't work like it used to. Strange...