parsingComputeLib doesn't build

[formrre]

parsingComputeLib doesn't build under some very specific conditions anymore, Holmake in compiler/parsing fails with: Don't know how to build necessary target(s): /home/user/cakeml/semantics/semanticsComputeLib.ui This happened, because semanticsComputeLib was moved into semantics/proofs. This can be potentially fixed by moving parsingComputeLib into parsing/proofs. Holmake -r cleanDeps doesn't help and I am failing to reproduce this even on a fresh clone

[formrre]

I have found a way to reproduce this. No idea why it doesn't happen in Holmake, doing load "parsingComputeLib"; interactively appropriately complains parsingComputeLib.sml:45: error: Structure (semanticsComputeLib) has not been declared, this is on a fresh clone.

[formrre]

This must be attempted before doing Holmake inside parsing/proofs as they share the same heap and semantics/proofs must not be built either as it shares heap with semantics.

[formrre]

@xrchz concerning your comments on #576, the other possible fixes I can think of are making parsing depend on semantics/proofs, reverting to the state before cleanup, where semanticsComputeLib was in semantics, but that would move namespaceProps back too, or just documenting the weird behaviour, I don't think any of these are ideal. EDIT: my mistake, termination is currently still in semantics

[mn200]

What is the route to reproduction from a clean checkout of master please?

[formrre]

@mn200 to reproduce the odd load behaviour do:

1. Holmake inside compiler/parsing on a clean checkout, it builds semantics, but not semantics/proofs, where the semanticsComputeLib currently is, doing load "parsingComputeLib"; interactively afterwards fails.
2. if you do Holmake inside semantics/proofs on a clean checkout and then try doing the load inside compiler/parsing everything works nicely.

This is because, semantics and semantics/proofs share a heap, if I understand correctly. I have no idea how to reproduce the Holmake failure on a clean checkout at the moment.

[mn200]

Thanks for the description of the failure. Given the dependency, there should be a link to semantics/proofs in the INCLUDES information for the compiler/parsing directory. If any of the script files in compiler/parsing attempted to use parsingComputeLib, then this would cause a failure.

Luckily (?), nothing actually ever uses parsingComputeLib and so the issue is moot. There are some obvious fixes:

1. delete parsingComputeLib because it's never used
2. put ../../semantics/proofs into the INCLUDES in compiler/parsing
3. move parsingComputeLib into compiler/parsing/proofs, which already has an INCLUDES-dependency on ../../semantics/proofs.

Perhaps @xrchz could make the call here. (Option 2 seems sub-par because it ties an “implementation” directory to a “proof” directory.)

[xrchz]

Is there also an option to remove the dependency? (My 4 below.)

I'm leaning towards option 1 otherwise, but I also see this as an opportunity to progress the observation in #321 that parsingComputeLib is not used where it ought to be.

I would probably veto option 3, and attempt to add some more options: 4. Make parsingComputeLib not depend on semantics ComputeLib -- I haven't looked into whether this is impossible. 5. Move semanticsComputeLib back to semantics somehow.

My preferences between them are something like: 4, 1, 2, 5 I know it looks bad to depend on a proofs directory in an implementation directory, but semantics/proofs is a special case: the semantics doesn't have an implementation/proofs split in the same way as the compiler does.

[mn200]

If there were a clear specification for what parsingComputeLib is supposed to do, your option 4 might be possible. At a guess, I suppose it's supposed to provide CBV_CONV-ability for parser calls, but do “parser calls” include cmlPtreeConversion functionality, for example? And who is the client for this?

Once the spec is nailed down, it would then be fairly straightforward to assemble the list of rewrites/definitions that would have to go into it. That needn't depend on semantics at all (any uses of cmlPtreeConversion functions could be explicitly handled in compiler/parsing).

But again, as Makarius might say, what is the actual desired application?

By the way, assembling computeLib lists of theorems in one place is a fragile methodology, as we see when theorems are deleted or replaced, and computeLib files then annoyingly break. I think theorem attributes would handle this better.

[xrchz]

The client is parse_topdecs or process_topdecs as mentioned in #321.

[mn200]

parse_topdecs requires evaluation of functions defined in semantics (those from ptreeConversion). I can pull in the appropriate definitions trivially enough, making it not depend on semanticsComputeLib. But then, that would seem to defeat the purpose of having a semanticsComputeLib. (It's easy to not depend on things if you just avoid the abstractions they provide and build your own copies.)

[xrchz]

Thanks for that info. We have now ruled out option 4, and I'd say we should also veto option 1 given the existence of parse_topdecs. Therefore, I suggest to take option 2: make compiler/parsing depend on semantics/proofs. (I said earlier why this isn't as bad as it looks: semantics are not like the implementation, and can all be considered proofs-like.)

[mn200]

This makes me wonder if we shouldn't just merge semantics and semantics/proofs.

Holmake handles big directories better than successive small ones too (at least for the moment).

[mn200]

Also: can you suggest/dictate a naming scheme for regression test files please? I want to test *computeLib files (obviously, those in semantics and parsing have never been so tested) and to do it soon after they're set up. Without a selftest.exe mechanism it seems easiest to just create a “test” theory to do this.

I do this in a separate test directory for the PEG.

[myreen]

Even if we merge parts, I hope we can retain the idea that:

• semantics is the definition of the source semantics, and
• semantics/proofs are proofs / general lemmas about the source semantics.

This is in line with how we separate the compiler definition from the compiler proofs.

[mn200]

Something has been mis-characterised if a computeLib is needed in semantics/proofs.

[xrchz]

Also: can you suggest/dictate a naming scheme for regression test files please? I want to test *computeLib files (obviously, those in semantics and parsing have never been so tested) and to do it soon after they're set up. Without a selftest.exe mechanism it seems easiest to just create a “test” theory to do this.

I do this in a separate test directory for the PEG.

The precedents I know of are

• compiler/parsing/tests/*TestsScript.sml (as you mentioned)
• compiler/inference/tests/*Script.sml
• translator/ml_translator_testScript.sml I think the tests directory with whatever theories you like in it is a good convention. If there's only one theory you can opt for the single _testScript.sml approach, but it doesn't scale as well in case someone wants to do more tests some day.

[xrchz]

Something has been mis-characterised if a computeLib is needed in semantics/proofs.

semantics/proofs defines new constants that need to be in a computeLib. For example, namespaceProps$alistSub. It also proves better equations for previously defined constants such as nsSub_compute_thm. I could perhaps be convinced that these things (there are a few more) should be moved back to namespaceTheory rather than namespacePropsTheory, and then the semanticsComputeLib could move up with them. How does that sound? (Would @SOwens object to this?)

[mn200]

If they need to be computed/evaluated (i.e., end up in the compiler), then it doesn't seem as if these constants should be in a proofs directory. Theorems about them, sure. But to be consistent with what happens under compiler/backend, computational content shouldn't be there.

[xrchz]

I agree that it's inconsistent with compiler, which could be confusing. But I think semantics really is different: the root directory is for the definition of the CakeML language (only), and the proofs is for extensions, helpers, and lemmas for working with the semantics. We could perhaps use a different name, or change this convention. I think proofs is ok though. Maybe extra would be better?

[xrchz]

Nitpick: needing to be computed/evaluated is not equivalent to ending up in the compiler. The translator and similar machinery can use the semantics this way.

[xrchz]

But perhaps the best thing to do is move all these definitions up into the semantics root. I'd love to get @SOwens to weigh in here.

[mn200]

Nitpick acknowledged!

We already have a tokenUtils in semantics; it seems to me that analogous names could be used for other theory-stems. Of course, it would probably be better still if we could just put the utility functions into the source .lem files, but lem is such a pain to use...

[xrchz]

What needs to be done to close this issue?

[mn200]

As per 4d95a4936d39, all of the parsing process's selftests execute with the custom compsets from parsingComputeLib. I think I need to make sure that parse_topdecs or whatever the cf entrypoint is called also uses this tech.

[xrchz]

All the parsing stuff to be replaced is in cfTacticsBaseLib.sml, I believe.

Actually, it's used in cfTacticsLib.sml, so ideally replace that call and remove the stuff from the base lib.