ijcar2020 branch fails to build

[paul-snively]

Steps to reproduce:

1. Create environment for ancient Coq and ancient OCaml with opam switch create coq8.4pl6 4.02.3
2. Use new environment with eval $(opam env)
3. Pin ancient Coq with opam pin add coq 8.4.6~camlp4
4. Clone repo with git clone git@github.com:mit-plv/fiat.git && mv fiat ijcar2020
5. cd ijcar2020
6. git checkout ijcar2020
7. Follow steps in README.rst
   1. export COQPATH=/home/psnively/ijcar2020/bedrock
   2. make -C bedrock -j4 facade qsfacade

Result:

make: Entering directory '/home/psnively/ijcar2020/bedrock'
make: *** No rule to make target 'Bedrock/reification/extlib.cmi', needed by 'reification'.  Stop.
make: Leaving directory '/home/psnively/ijcar2020/bedrock'

I've tried examining the build system to see if I could correct the issue myself, and given up. I'm very interested in this work, but I have to say I'm extremely concerned about its being so terribly out-of-date with respect to Coq's evolution, its dependence on "vendored" third-party OCaml libraries such as extlib, its lack of integration with OPAM, and its highly magical and therefore version-dependent "wiring together" of Coq and OCaml code by means of Lovecraftian approaches to software engineering. There Has Got To Be A Better Way™, and I strongly urge your team to find it.

[cpitclaudel]

Thanks for the report — looks like I messed up something with packaging :/ I'll fix it.

I'm very interested in this work, but I have to say I'm extremely concerned about its being so terribly out-of-date with respect to Coq's evolution

Yes, it's a real problem. The transition to Coq 8.5 broke a lot of stuff, and the Coq devs who tried to help us port Bedrock didn't succeed to. The non-bedrock parts of this work were mostly compatible with later versions of Coq, but the motivation to support them was low given that Bedrock itself couldn't be ported.

We're currently working on new iterations of this code, built on a more robust and modern base (we're targeting bedrock2, unsurprisingly). Things are still very early, but you can have a look at https://github.com/mit-plv/rupicola/. (As you might imagine, it's no fun working with outdated tools, and we don't do it out of a dedication to staying in the dark ages)

its dependence on "vendored" third-party OCaml libraries such as extlib

Oh, I think there's a bit of confusion here. extlib.ml isn't the OCaml library extlib, AFAIK (it's just a small Coq plugin). I agree the name collision isn't ideal, but I don't think that's an example of a vendored library.

and its highly magical and therefore version-dependent "wiring together" of Coq and OCaml code by means of Lovecraftian approaches to software engineering.

I'll admit that I don't know a much better way when it comes to writing plugins for Coq (but don't quote me on this: all of these things are in the Bedrock repo, which I didn't really touch for this project).

Dune has a much nicer story about mixing OCaml and Coq, but the support for that has only been available for a few months at this point.

[cpitclaudel]

Ah, it's a silly issue :/ I screwed up the submodule setup when I created the branch. I'll push a fix, but let me make sure that I didn't make another silly mistake first. Thanks again for the report.

[paul-snively]

@cpitclaudel, thanks so much for your prompt attention, and I'm glad to hear my report may have helped move the ball forward in some small way.

On that note, let me apologize for the intemperate tone of my report. In retrospect, I expressed my frustration too forcefully.

The transition to Coq 8.5 broke a lot of stuff, and the Coq devs who tried to help us port Bedrock didn't succeed to.

I would think, frankly, that this would cause an immediate halt on further work with Bedrock, with an eye towards a post-mortem and a "let's not do that again at all costs" point of view on new work. I know Adam, in particular, is keen to have Coq seen as a practical tool for certified software development—hence all of this work!—but it's a hard sell when things are so finicky about versions and even the developers of the primary tool can't help.

We're currently working on new iterations of this code, built on a more robust and modern base (we're targeting bedrock2, unsurprisingly).

I presume this is an effort in the spirit that I just alluded to. I will have to look more closely, but let's just say I hope it's methodologically significantly different than Bedrock, so as not to fall prey to exactly the same sorts of sensitivity to versions you're suffering from now.

Oh, I think there's a bit of confusion here. extlib.ml isn't the OCaml library extlib, AFAIK (it's just a small Coq plugin). I agree the name collision isn't ideal, but I don't think that's an example of a vendored library.

Ah, my mistake. Thanks for pointing it out!

I'll admit that I don't know a much better way when it comes to writing plugins for Coq (but don't quote me on this: all of these things are in the Bedrock repo, which I didn't really touch for this project).

To me, this is the crux of the issue: Coq doesn't have a "plugin API." So the moment you find yourself thinking "I'll write some OCaml code to link into Coq," it's really time to stop and ask:

1. Are we using the right tool for the job? Maybe Coq isn't it!
2. Is there an alternative implementation strategy?

I see that at least some thought has been given to the latter, in the sense that "reification" can be implemented with the OCaml code or (very slowly) with Ltac. But I can't help but wonder whether one of the other approaches to proof automation in Coq wouldn't serve everyone better:

1. coq-elpi, in which reification is an explicit example use-case.
2. MetaCoq, where reification is the first bullet-point use-case for the Template-Coq system.
3. Mtac2, which focuses on being a "typed tactic language," but is an extension of the previous work on Mtac, which includes reification as a feature.

To be clear, I am spitballing, not having used the above tools in anger, nor having developed anything as ambitious as Bedrock.

Thanks again for your prompt reply, and I hope your correction applies successfully, :-)

[cpitclaudel]

On that note, let me apologize for the intemperate tone of my report. In retrospect, I expressed my frustration too forcefully.

Thanks for your kind message. No worries — it's quite frustrating when things don't build (and I should have checked this better. It took a while to get the paper published, so things went through multiple iterations that made it a bit trickier to keep track.

I would think, frankly, that this would cause an immediate halt on further work with Bedrock

This is a good summary of what happened: Bedrock development stopped, and work on Bedrock2 started with a more restricted scope and no dependence on OCaml plugins

Are we using the right tool for the job? Maybe Coq isn't it! Is there an alternative implementation strategy?

These are all reasonable questions. I think the answers differs slightly if we're trying to answer questions like "can we build a prototype of X with proofs" versus questions like "will we get a robust X out of this". I ask the former when starting a research project, and the latter when starting a software one, and often but not always I get to answer both positively (for example, we've done a lot of packaging and tooling work on Koika, our hardware compilation project).

But sometimes experimentation without an eye to building rock-solid stuff in the short term is valuable too: you start by focusing on the first question, and after a few iterations you settle on something, and then you can answer the second question.

Thanks again for your prompt reply, and I hope your correction applies successfully, :-)

Yup, working on it :)

[cpitclaudel]

Thanks again for the report. As I mentioned above, it turned out to be a very silly thing: I messed up the module configuration when cutting the ijcar20 branch. Everything builds fine for me now. I think I'll try to package a VM when I have a bit more time, to make things a touch more reproducible. Thanks again for the report —- much appreciated.