Using menhir --explain

[thierry-martinez]

Before dune.3.0, with the following stanza,

(menhir (modules ...) (flags --explain))

when the menhir grammars have conflicts, the reports that menhir generates to describe the conflicts (.conflicts files, one for each .mli file) were available in _build/$profile/.

Since dune.3.0, sandboxing prevents dune from keeping these files, forcing the user to run menhir --explain manually in the source tree to get the reports.

Desired Behavior

The .conflicts files could be copied to the _build/$profile/ directory: that would restore the previous behavior (before dune.3.0), which was better than the current situation, even if I would prefer never have to touch to the ``_build/` directory.

Another behavior could be to promote the .conflicts files in the source tree, which would be close to the experience of using menhir without dune, and which would made the .conflicts file easier to notice. Another possibility could be to dump these files to the standard output when they exist (which can be convenient, but with the same drawbacks than with warnings, that are not displayed again in case of rebuild).

Example

A file test.conflicts should be available somewhere (or its contents should be displayed) after compiling the following file.

test.mly:

%token A
%start<unit> a
%%
let a := A; {} | A; {} 

dune:

(library (name test))
(menhir (modules test) (flags --explain))

This issue was previously discussed here: https://discuss.ocaml.org/t/how-to-use-menhir-explain-with-dune/11132

[Alizter]

You can disable sandboxing with --sandbox none. Does that work?

[rgrinberg]

Promoting it doesn't seem right as it seems like a file with error messages/diagnostics. I wonder why menhir doesn't just dump this output into stderr? @fpottier Why is the separate file necessary?

[thierry-martinez]

@Alizter, thank you for the tip: indeed, --sandbox none works (.conflicts files are available in _build/$profile). I think I would still prefer not to have to disable sandboxing to get these files.

[thierry-martinez]

@rgrinberg, indeed, these are diagnostics. Piping them to stdout/stderr would be an option, but what would be the right place with dune for storing such files with errors or diagnostics if not in the source tree? Storing them in _build/ looks a bit arcane.

[nojb]

Promoting it doesn't seem right as it seems like a file with error messages/diagnostics. I wonder why menhir doesn't just dump this output into stderr? @fpottier Why is the separate file necessary?

This was also the behaviour of "yacc" tools. I think the reason is that this output can be rather large so it is not very useful to read them on the console; one would rather use a text editor.

Thinking out loud, what about making this file an explicit output of the Menhir rules?

[rgrinberg]

This was also the behaviour of "yacc" tools. I think the reason is that this output can be rather large so it is not very useful to read them on the console; one would rather use a text editor.

Right, but I think we already talked about saving the stderr output of compilation commands to replay warnings. I would imagine this to apply to menhir commands as well. In which case, it would be possible to browse the output with the editor.

[Lelio-Brun]

@Alizter, thank you for the tip: indeed, --sandbox none works (.conflicts files are available in _build/$profile). I think I would still prefer not to have to disable sandboxing to get these files.

Strangely it does not work in my use case, using dune 3.7.1, either with dune build or dune exec.

[Alizter]

@Lelio-Brun is the command running? Can you check what --always-show-command-line says and check any related _build directories?

[Lelio-Brun]

> dune build --sandbox=none --always-show-command-line
File "src/dune", line 7, characters 0-45:
7 | (menhir
8 |  (modules parser)
9 |  (flags --explain))
(cd _build/.sandbox/9796...938b/default && /home/xxx/_opam/bin/menhir --explain src/parser.mly --base src/parser --infer-read-reply src/parser__mock.mli.inferred)

Thanks, so two remarks:

1. The file parser.conflicts is indeed present in the sandbox 979...938b
2. Removing --sandbox=none produces exactly the same outcome

[Alizter]

It is strange that --sandbox none did nothing here. @rgrinberg any ideas what might be happening?

[rgrinberg]

Isn't it just stale artifact deletion? Dune would delete conflicts file because it doesn't know it's a target.

[Alizter]

@rgrinberg But in this case the output of --always-show-command-line says it used a sandbox even though --sandbox none was passed. Shouldn't this be run directly in _build/default?

[Alizter]

Anyway, here is a fix #7607

[gasche]

I came up here after trying to use (flags --explain) in a Menhir-using project.

Here is my understanding of the situation:

• dune is currently unable to produce conflict-explanation files; this is a big deal for Menhir uses
• one workaround is to pass --sandbox none, and then look in the _build output
• @Alizter proposed a fix in menhir: support for .conflicts targets when passing --explain #7607, but run into tricky questions and eventually closed his own issue ("this needs menhir expertise")
• @Tchou proposed another fix in fix: keep menhir .conflicts files (#6865) #9025, which is still a draft ("this needs dune expertise")

[gasche]

Further comments.

1. Both PRs rely on checking whether the --explain flags was passed to Menhir. I know little about Dune but this sounds weird to me. Why not introduce a new (explain) field in the menhir stanza, if we want to special-case the build system behavior?

2. Menhir in general relies on options that generate new files -- and I am sure that many other metaprogramming tools follow the same UI pattern. It would be nice if Dune sandboxing could be taught to run the menhir command in a clean subdirectory (with just the parser file and possibly other dependencies specified by in the (menhir ...) stanza), and preserve the whole subdirectory somewhere in the build artifacts (for example: foo.mly.objs/). The build system may not be aware of some of the files produced, but this is fine as long as they are only outputs.

[Alizter]

Both PRs rely on checking whether the --explain flags was passed to Menhir. I know little about Dune but this sounds weird to me. Why not introduce a new (explain) field in the menhir stanza, if we want to special-case the build system behavior?

We essentially already have that in #9025. The issue is that we are trying to support users passing --explain from an env stanza in their dune-workspace file. If we had an (explain) field, users would have to edit their menhir stanzas directly rather than being able to tweak the environment in developer mode. It might also cause confusion if they end up passing --explain and it doesn't work.

Menhir in general relies on options that generate new files -- and I am sure that many other metaprogramming tools follow the same UI pattern. It would be nice if Dune sandboxing could be taught to run the menhir command in a clean subdirectory (with just the parser file and possibly other dependencies specified by in the (menhir ...) stanza), and preserve the whole subdirectory somewhere in the build artifacts (for example: foo.mly.objs/). The build system may not be aware of some of the files produced, but this is fine as long as they are only outputs.

This could be an option. Rather than having case-by-case rules in the menhir implementation, we could simplify it and have menhir produce a directory target for each use case. This would avoid us having to specify each target. I believe menhir rules were added before directory targets were in a usable state, but I don't see any problems having such a feature now.

We discussed doing something similar with Coq's extraction feature, which is similar in menhir in the way the rules are written.

@emillon Does having menhir rules produce directory targets sound like a viable solution?

[gasche]

The issue is that we are trying to support users passing --explain from an env stanza in their dune-workspace file

But apparently this makes the implementation more complex, and the end result is that we don't have the feature. I appreciate that you did all this effort, but I would rather have something simple that works.

[ejgallego]

Why not introduce a new (explain) field in the menhir stanza, if we want to special-case the build system behavior?

Indeed that seems a good idea, barring other more optimal (but also complex) solutions. This is a very important feature, and the (explain) field can be implemented in 30 mins.

[nojb]

• Why not introduce a new (explain) field in the menhir stanza, if we want to special-case the build system behavior?

I gave this one a try: #9512.