Tutorial doesn't tie examples to their names in the actual code

[tlringer]

Another thing I am struggling with as I go through the tutorial is actually finding each example. For example, for the second example, I had to search for it to even find the function:

(base) talia@xenon-v4:~/cn-tutorial/build$ grep -R "doubled" ./exercises
./exercises/slf1_basic_example_let.signed.c:int doubled (int n)

which I needed because I am running things as I go and trying to tweak specifications and so on myself. It would be nice if the tutorial explicitly stated the name of the file containing each example as it went through each of them.

[bcpierce00]

Yes, this has been an ongoing irritation.

For the moment, please feel free to add file names as comments at the top of the file. This is not a long-term solution, but it will take us some distance.

At some point we may want to switch documentation processors, but in the shorter term maybe a simpler hack would suffice: Suppose we pre-processed the .adoc file before sending it through asciidoc and auto-generated appropriate filename annotations? Crude, but effective.

@cp526 Does that seem reasonable?

[cp526]

Agreed. We used to have those filenames, and then they got lost when we transitioned from an m4-preprocessed markdown file (which had some tiny bit of machinery for this) to asciidoc to make includes more reliable.

@bcpierce00 That sounds good to me. And also agreed we may want to move to some other documentation processor at some point. The one advantage asciidoc has over markdown for us is that it has a "native" include directive. But I'm not attached to this setup (and asciidoc's syntax is a bit awkward sometimes).

[bcpierce00]

For the short term, if someone has a clean way to add a one-liner to the makefile to translate

[source,c]

include::exercises/0.c[]

into

++++

exercises/0.c

++++ [source,c]

include::exercises/0.c[]

before running asciidoc, I think that would get us going just fine for now.

On Thu, May 23, 2024 at 4:58 AM Christopher Pulte @.***> wrote:

Agreed. We used to have those filenames, and then they got lost when we transitioned from an m4-preprocessed markdown file (which had some tiny bit of machinery for this) to asciidoc to make includes more reliable.

@bcpierce00 https://urldefense.com/v3/__https://github.com/bcpierce00__;!!IBzWLUs!UOw9UzNW9pKSsTroM8Lv2W6RD1XdwnH05dgMJb72-cBCSQt1Be2cd9ZiWYd87PrwNuGRmqTuoQLE0l4LDlqLeeyncEgr$ That sounds good to me. And also agreed we may want to move to some other documentation processor at some point. The one advantage asciidoc has over markdown for us is that it has a "native" include directive. But I'm not attached to this setup (and asciidoc's syntax is a bit awkward sometimes).

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cn-tutorial/issues/17*issuecomment-2126587247__;Iw!!IBzWLUs!UOw9UzNW9pKSsTroM8Lv2W6RD1XdwnH05dgMJb72-cBCSQt1Be2cd9ZiWYd87PrwNuGRmqTuoQLE0l4LDlqLeaZkr1bV$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQCZRTFQYWIW4SANBISLZDWVSZAVCNFSM6AAAAABID6A4SGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMRWGU4DOMRUG4__;!!IBzWLUs!UOw9UzNW9pKSsTroM8Lv2W6RD1XdwnH05dgMJb72-cBCSQt1Be2cd9ZiWYd87PrwNuGRmqTuoQLE0l4LDlqLeR76j10N$ . You are receiving this because you were mentioned.Message ID: @.***>

[cp526]

Thanks for the suggestions. If I got it right, this should be fixed now (assuming the sed script behaves the same on Mac and non-Mac systems).