New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Remove liquid-base with automatic search of assumptions #2166
Conversation
Also deletes mirror-modules, hopefully not needed anymore.
d25574f
to
2b43377
Compare
Looks like there is some speed up in CI with these changes. While circleci jobs in But I don't have insights about why. One factor could be that assumptions fit in 33 modules while the removed |
Very likely - it used to take a while for GHC to just “compile” those
wrapper packages
On Fri, Apr 14, 2023 at 6:51 PM Facundo Domínguez ***@***.***> wrote:
Looks like there is some speed up in CI with these changes. While circleci
jobs in develop take 30 minutes. Jobs in this branch are closer to 20
minutes. I've also noticed some speed ups locally.
But I don't have insights about why. One factor could be that assumptions
fit in 33 modules while the removed liquid-base holds more than 200
modules.
—
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/pull/2166*issuecomment-1509458057__;Iw!!Mih3wA!Ad0O1LzN9zdcRq6nLVXWocZmTuOOvzp2JMmHuRx4d8GIjMQvNAUtOXKmIKju3iLAfw-IZPvEXomK9aK1MaC7I9dg$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4ODTYKET3OCNZHO65ITXBH5LFANCNFSM6AAAAAAW5ZMNQY__;!!Mih3wA!Ad0O1LzN9zdcRq6nLVXWocZmTuOOvzp2JMmHuRx4d8GIjMQvNAUtOXKmIKju3iLAfw-IZPvEXomK9aK1MWaAszhz$>
.
You are receiving this because your review was requested.Message ID:
***@***.***>
--
- Ranjit.
|
3944be8
to
4e50845
Compare
6e6d778
to
bf476e1
Compare
3ea61d2
to
56e9e9c
Compare
@nikivazou, @ranjitjhala, in the absence of objections, I would be merging this in a couple of days. Please, let me know if you'd like to offer more review time. |
Good idea! |
Use LHAssumptions for the other liquid-* packages
🎉🎉🎉
On Thu, Apr 27, 2023 at 7:02 AM Facundo Domínguez ***@***.***> wrote:
Merged #2166
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/pull/2166__;!!Mih3wA!BJ-6c0LBCAg9YsqK6GFOts3A8R3fEVhCiAwv7elGam2t_DwPIlF9By5_YXpB1INtJCUW4_9S_HuxDSsbs3K5Ea7F$>
into develop.
—
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/pull/2166*event-9115015423__;Iw!!Mih3wA!BJ-6c0LBCAg9YsqK6GFOts3A8R3fEVhCiAwv7elGam2t_DwPIlF9By5_YXpB1INtJCUW4_9S_HuxDSsbs4QGK7vp$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OHJ3JQTPSFLGLFHLYLXDJ37ZANCNFSM6AAAAAAW5ZMNQY__;!!Mih3wA!BJ-6c0LBCAg9YsqK6GFOts3A8R3fEVhCiAwv7elGam2t_DwPIlF9By5_YXpB1INtJCUW4_9S_HuxDSsbs5wmrZuM$>
.
You are receiving this because you were mentioned.Message ID:
***@***.***>
--
- Ranjit.
|
This PR
liquidhaskell
package toliquidhaskell-boot
liquidhaskell
that reexports the plugin and additionally defines modules with assumptions forbase
andghc-prim
.Matching of modules is done solely by name. Whenever the target module imports module
A.B.C
, LH will try to load assumptions from moduleA.B.C_LHAssumptions
in dependency packages. It cannot load assumptions automatically from the home package, butA.B.C_LHAssumptions
can be imported manually as well.This PR implements much of #2106. If the approach looks good, I will proceed to remove the remaining
liquid-*
packages and then I'll update the documentation.