Bas Spitters (Jun 15 2020 at 20:37): Bas Spitters (Jun 15 2020 at 20:37):Not much seem to be happening here, but I think combining with Equations is an interesting direction
https://github.com/antalsz/hs-to-coq/issues/138
Yao Li (Jun 16 2020 at 20:39):Indeed! I would be excited to learn what would happen combining with Equations.
Yao Li (Jun 16 2020 at 20:42):@Wolfgang Meier Not sure if you have started working on this. Please feel free to ask if you have any questions, and let us know if you have any discoveries!
Wolfgang Meier (Jun 20 2020 at 17:25):Thanks for asking. At the moment I only have a small proof of concept, that works for very simple functions, which is not good enough to show yet.
A general question:
Replacing 'Program Fixpoint' with 'Equations' will break existing setups (as expected, due to different obligations).
I assume, we want to avoid this (?).
-> As a solution I thought of adding an edit like 'translate to equations <functionname>'. What do you think?
Yao Li (Jun 20 2020 at 19:30):I think that is a great idea.
I may be wrong, but I think it's possible that there are features that we want but not yet supported by Equations (for example, I don't know how to add universe variables to Equations). I think it's a great idea to roll out Equations support as a optional feature that can be turned on and off at the functional level and the module level. And maybe some time in the future we can consider setting translating to Equations as the default option.
Wolfgang Meier (Sep 15 2020 at 07:40):Hello @Yao Li
Regarding #138
I'm currently doing some more testing, will probably submit a PR next week or so.
I was wondering, what do you think about adding Equations as a general dependency? (e.g. directly in Preamble.hs)
Yao Li (Sep 15 2020 at 15:43):That's exciting news!
As for the question, I'm actually not so sure. I personally prefer leaving Equations out of base for now to keep it simple and not depending on anything else other than Coq standard library, but I can see some potential arguments for having Equations as a general dependency: for example, maybe Equations would make base functions more readable and look more like Haskell.
Is there a particular reason you want to use Equations directly in Preamble.hs? And since I'm not an expert on Equations, I wonder if you have observed some additional benefits of combining Equations with hs-to-coq? And you want it as a general dependency because there is a particular function in Preamble that calls for Equations, or do you plan to use Equations broadly?
Tadeusz Litak (Sep 17 2020 at 12:35):is there any specific reason why hs-to-coq refuses to work with anything else than 8.10? By now it is a totally obsolete version. Yet example/boot.sh in line 11 says COQ_VERSION=8.10. Why? What is the problem for 8.11 and 8.12?
Karl Palmskog (Sep 17 2020 at 12:39):I would argue 8.10 is still fairly modern compared to what a lot of Coq projects are using. A quick look says that hs-to-coq is using obsolete code from the 8.10 Stdlib that has been completely removed in 8.11 and later.
Karl Palmskog (Sep 17 2020 at 12:40):in other words, refactoring is possible but will likely be some work and break backwards compatibility
Yao Li (Sep 17 2020 at 15:59):Karl is right for the reasons.
We do have a coq-8.11 branch though, which solves the problem and works on Coq 8.11. We did not merge it in master yet because of the backwards compatibility issue (it's unfortunate that the same code works 8.11 does not work for 8.10).
Yao Li (Sep 17 2020 at 15:59):https://github.com/antalsz/hs-to-coq/tree/coq-8.11
Wolfgang Meier (Sep 25 2020 at 05:56):It turns out, using Equations didn't really help us in what we were trying to do.
If you're interested, you can take a look at https://github.com/womeier/hs-to-coq/tree/equations and tell me if you're ok with the AST changes I made.
A few more things are left to do, but I don't have time for this right now, can't tell when/if I will, will not submit a PR for now.
Yao Li (Sep 25 2020 at 21:46):Thank you @Wolfgang Meier for the update! I am also a bit occupied at the moment but I'll take a look at it when I can!
Bas Spitters (Sep 26 2020 at 11:10):@Wolfgang Meier I'm curious what did you expect from Equations that wasn't there?
Yao Li (Sep 27 2020 at 01:20):@Bas Spitters I know one motivation might be (to my understanding) the way we translate Haskell mutual fixpoints produces code duplications (see https://github.com/antalsz/hs-to-coq/issues/162). For certain parts of GHC, the translation would result in very large Coq files. There might be other motivations I'm not aware of.
Wolfgang Meier (Sep 28 2020 at 05:43):We have a generated mutually recursive function (with 3 fix-definitions) that we can't compile due to stack overflow issues. We thought Equations would help with performance, but until now it wasn't enough.
Bas Spitters (Sep 28 2020 at 07:13):Interesting. "Can't compile" in Coq. It would probably help reporting those issues.
Bas Spitters (Sep 28 2020 at 07:16):@Yao Li It's been a while since I've looked at the hs-to-coq paper, but one could imagine that it would help with 3.4 and 3.7 here:
https://arxiv.org/abs/1711.09286
Yao Li (Sep 28 2020 at 19:43):Yes it would be interesting to see if Equations can help with those examples. Some other benefits are also recorded here by Josh Cohen: https://github.com/antalsz/hs-to-coq/issues/138 When I have more time, it might be fun to make some comparisons of how hs-to-coq did certain things, how Equations did certain things, and what Equations might help us.
Last updated: Feb 06 2023 at 07:03 UTC