Quinn (Nov 02 2021 at 12:26): Quinn (Nov 02 2021 at 12:26):in examples/containers/Makefile, there is a module order, and the behavior of hs-to-coq is dependent on the order. Is there a tool of some kind for getting the dependency graph and flattening it into what the module order ought to be?
Karl Palmskog (Nov 02 2021 at 12:33):coqdep is the reference implementation of Coq file dependency extraction. Some people build scripts on top of coqdep to build .dot files and the like: https://gitlab.inria.fr/flocq/flocq/-/blob/master/Remakefile.in#L97
Quinn (Nov 02 2021 at 12:44):ok cool, but I think I need the haskell version of coqdep
Karl Palmskog (Nov 02 2021 at 12:45):there isn't any, to my knowledge. And if there is, it has to play catch-up to coqdep constantly
Quinn (Nov 02 2021 at 12:46):glancing at this i'm not so sure there's one solution, rather I must have an opinion or taste to select from multiple solutions. I'm curious what the hs-to-coq-containers paper authors used.
Quinn (Nov 02 2021 at 12:47):looks like SourceGraph is dead
Quinn (Nov 02 2021 at 13:00):I know from experience that tree -ifF to start, then nudging the permutation until the hs-to-coq-invoking make process stops complaining will get you there, but there ought to be a better way.
Stephanie Weirich (Nov 02 2021 at 13:08):So far, we've untangled dependencies by hand. It would be good to have mechanical assistance for this task.
Quinn (Nov 03 2021 at 01:35): Li-yao (Nov 03 2021 at 14:19):ghc itself is able to figure out dependencies so I imagine we can coopt that functionality from the ghc lib somehow.
Quinn (Nov 03 2021 at 16:11):Have yall talked about scripting for hs-to-coq Makefile generation, to generate something like examples/containers/Makefile? A cli, maybe a config to pass in that has a yaml mapping of .hs files to edits files and preamble.v files. just spitballing here. https://hackage.haskell.org/package/makefile
Quinn (Nov 03 2021 at 16:13):I'm assuming doubling down on make makes sense, since the coq ecosystem is so riddled with make. but it's possible that .sh files would be better. I'm uncertain, but I'm getting more experience with hs-to-coq as a user so I hope to have an informed opinion soon.
Karl Palmskog (Nov 03 2021 at 16:16):the Coq ecosystem is undergoing a transition from Make to Dune. Most projects are already using Dune to build all their OCaml files, including Coq itself, and some have switched to using Dune for the Coq parts too
Quinn (Nov 03 2021 at 16:18):roger that, I had no idea!
Karl Palmskog (Nov 03 2021 at 16:18):but this change is orthogonal to using coqdep, both projects that use Dune and Make use coqdep under the hood
Karl Palmskog (Nov 03 2021 at 16:20):please see here for a breakdown of build/packaging tools we use: https://github.com/coq-community/awesome-coq#package-and-build-management
Quinn (Nov 03 2021 at 16:20):right. but on the subject of "building out a dev cycle for hs-to-coq", the dune point you made is crucial
Karl Palmskog (Nov 03 2021 at 16:21):Dune and Make builds can in fact live side by side in many cases, here is an example project I made which does that: https://github.com/palmskog/coq-program-verification-template (this project does C verification in Coq using VST in a similar way to what I think you want for hs-to-coq)
Emilio Jesús Gallego Arias (Nov 03 2021 at 17:05):Hi folks, not sure if I follow, but it should be pretty easy to have a small script that takes the output of ghc -M and translates it to dune rules
Emilio Jesús Gallego Arias (Nov 03 2021 at 17:06):or not sure you would even need to do that, I guess so you can maybe indeed get a complete compositional build if you are generating your binary with an OCaml rule
Emilio Jesús Gallego Arias (Nov 03 2021 at 17:06):let me know if I can be of help, coqdep output is simlar to ghc -M so this is how we first implemented compilation support for Coq's .v files
Karl Palmskog (Nov 03 2021 at 17:13):(maybe relevant: Emilio is the co-maintainer of Dune support for Coq)
Emilio Jesús Gallego Arias (Nov 03 2021 at 17:24):Emilio Jesús Gallego Arias said:
or not sure you would even need to do that, I guess so you can maybe indeed get a complete compositional build if you are generating your binary with an OCaml rule
What this obscure phrase means is that whenever you update your hs-to-coq toolchain, the examples get recompiled too
Karl Palmskog (Nov 03 2021 at 17:25):and I think you should say "locally", since one would normally rebuild everything in CI regardless
Emilio Jesús Gallego Arias (Nov 03 2021 at 17:25):Yup, I mean while developing
Emilio Jesús Gallego Arias (Nov 03 2021 at 17:26):In dune rules are of the form {deps} ---[action]---> {targets} , but indeed if action is for example "run coqc" , dune will track coqc as a dependency and re-run the rule if it changes
Emilio Jesús Gallego Arias (Nov 03 2021 at 17:27):Dune 3.0 even tracks system-wide binaries if you want, so for example would your gcc be updated, the required rules are re-run
Karl Palmskog (Nov 03 2021 at 17:28):aha, but when can we get tactic-to-Coq deps, so that changes to an OCaml tactic in Coq or Coq plugin triggers rebuild of all Coq files that explicitly or implicitly uses tactic? I think the limit is somewhere there right now...
Last updated: Feb 06 2023 at 05:03 UTC