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

Indeed! I would be excited to learn what would happen combining with Equations.

@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!

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?

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.

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)

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?

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?

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.

in other words, refactoring is possible but will likely be some work and break backwards compatibility

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).

https://github.com/antalsz/hs-to-coq/tree/coq-8.11

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.

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!

@Wolfgang Meier I'm curious what did you expect from Equations that wasn't there?

@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.

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.

Interesting. "Can't compile" in Coq. It would probably help reporting those issues.

@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

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