Clarifications about possible errors in the specification

[alessiofaieta]

I think I found some possible errors/typos in the specification, but I'm not sure about them. I suppose that creating issues on the repository would be a bit overkill, so is it okay if I ask clarifications about them here in the Discussions?

If yes, does it make sense if I ask them as separate comments to this post, in order to avoid spamming many small questions as separate posts?

If they turn out to be errors, I'm willing to submit pull requests to fix them (assuming I'm able to fix them).

[alessiofaieta]

If that's fine, in order to reduce round-trip time in the answers, I'll start asking the first one.

In section Structure > Instructions > Aggregate Instructions, the second parameter for instructions struct.get and struct.set is an u32, should it be fieldidx?

Reasons:

• by searching for fieldidx in the PDF, the definition of fieldidx from section Structure > Modules > Indices does not seem to be used;
• the definition of the text format for struct.get and struct.set in section Text Format > Instructions > Aggregate Instructions uses fieldidx instead of u32.

[rossberg]

Asking here is no problem. Please feel free to open issues or PRs as well as you see fit.

Fieldidx is defined to be u32, so technically it makes no difference. But I agree that stylistically, the uses should match up in different parts of the spec. (Another part to adjust could be the binary format, which also uses u32 and doesn't even define fieldidx.) If you want to create a PR, I'm happy to review it.

[rossberg]

Odd, those shouldn't be there, they are intermediate files that make is supposed to remove. Perhaps remnants of failing make runs? Perhaps try make distclean in the test-splice directory and run make test again.

[alessiofaieta]

Yes, at some point I killed the make run because it was taking a lot longer than usual, it seemed to be stuck when running the test-splice tests. After that I run make clean but apparently it wasn't enough. Doing as you suggested solved the problem, thanks.

[alessiofaieta]

Hi, I submitted pull request #2149 to fix this but I noticed that it hasn't been merged yet, I don't know if it's because some CI checks were not successful (it seems that CI failed to fetch a dependency). It's not my intention to put pressure on you, I just wanted to know if you were expecting me to do something about it.

[rossberg]

Oh, sorry, I must have missed that one. Will take a look.

[alessiofaieta]

No problem, thank you!

[alessiofaieta]

In the section about validation of instruction sequences, the title Empty Instruction Sequence: 𝜖 seems out of place, since the following rules also talk about non-empty instruction sequences. Does it have to be removed?

[rossberg]

Right, that heading should be removed.

[alessiofaieta]

In the modules syntax, the nonterminal symbol type links to Recursive Types, but I think that it should link to Modules > Types, since all the other nonterminals of modules link to the corresponding section under Modules.

[rossberg]

Agreed!

[alessiofaieta]

Nice! I tried to understand what might be influencing this behavior, but the problem is that it's not clear to me how references to sections work (sorry for not making this clear from the beginning haha). Could you provide some pointer to some reference that explains how they work? Or could you directly provide a suggestion on how to fix this? If it's faster for you to just fix it and you prefer to do it yourself then please do, otherwise I'd be happy to do it.

[rossberg]

The Latex that is generated simply uses macros, and those are defined in document/core/util/macros.def, cross-referencing the respective Sphinx docs + labels. For example, it currently says

.. |type| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{type}}

That should probably be

.. |type| mathdef:: \xref{syntax/modules}{syntax-type}{\X{type}}

[alessiofaieta]

It worked! Thank you :)

BTW, I just noticed that a commit from yesterday introduced a duplicate definition for vdashcontext in that same file (here), resulting in the following error (even though the compilation succeeds):

util/macros.def:1779: ERROR: Duplicate substitution definition name: "vdashcontext". [docutils]

If that's ok, I will remove it in the same pull request.

[rossberg]

Strange, yes, feel free to remove.

[alessiofaieta]

In the title of the section about the operational semantics of the if instruction (here), an else is missing. Is that on purpose?

[rossberg]

No, that appears to be a bug in the prose generator, which generates these headings. It somehow loses part of SpecTec's mixfix syntax. Unfortunately, that isn't straightforward to fix; can you open an issue for it, so I can triage it?

[alessiofaieta]

Got it, I had the impression that it wasn't a straightforward fix when I tried to dig into it, I'll open an issue.

[alessiofaieta]

In section Rolling and Unrolling, is the definition of expand() missing?

[rossberg]

Well, sort of. The expanddt function was actually obsolete and should have been inlined into the Expand rule. Done in the latest commit.