Open amigalemming opened 7 months ago
That could be possible. We need to agree whether the .liquid
directories should be placed, e.g. next to the interface files by default, and whether the user needs to be able to change the default.
I think its fine to just dump in the dist/
tbh - as long as the user knows where they are its ok?
Here are the locations of interface files. They are rather intricate because they depend on the compiler version, the architecture, and the package they belong too.
dist-newstyle/build/x86_64-linux/ghc-9.8.1/liquid-prelude-0.9.2.8.1/build/Language/Haskell/Liquid/List.hi
liquid-prelude/.stack-work/dist/x86_64-linux-nix/ghc-9.8.1/build/Language/Haskell/Liquid/List.hi
These bits of information seem relevant. I don't think we want to confuse the .liquid
files belonging to different packages.
If the user wants a different location we could provide a flag like -fplugin-opt=LiquidHaskell:output-dir=/path/to/output
which is absolute or relative to the current working directory of the compiler.
How would this work if we wanted to e.g. run a single file through LH?
On Wed, May 22, 2024 at 1:53 PM Facundo Domínguez @.***> wrote:
Here are the locations of interface files. They are rather intricate because they depend on the compiler version, the architecture, and the package they belong too. Locations for stack further depend on the particular snapshot used to verify the modules.
dist-newstyle/build/x86_64-linux/ghc-9.8.1/liquid-prelude-0.9.2.8.1/build/Language/Haskell/Liquid/List.hi
.stack-work/install/x86_64-linux-nix/5d56c9dbbd66414befbbca885ad575367e2995e031ccfba3533cf70bf9b5c100/9.8.1/lib/x86_64-linux-ghc-9.8.1/liquid-prelude-0.9.2.8.1-INWPGSaRg3lB73GWlUcrJG/Language/Haskell/Liquid/List.hi
These bits of information seem relevant. I don't think we want to confuse the .liquid files belonging to different packages or snapshots.
If the user wants a different location we could provide a flag like -fplugin-opt=LiquidHaskell:output-dir=/path/to/output which is absolute or relative to the current working directory of the compiler.
— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2278*issuecomment-2125726041__;Iw!!Mih3wA!AAWj8yKpP6mmsoDF-8Taol8M6UzfrJW4ld8Vv9siiYq50VqAQildtkdg3_KcQf15dmwCgA-o6itbdhB7gPYUgS6R$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OFK3UAUYISF3PKY3HLZDUAVFAVCNFSM6AAAAABFWWWKJSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMRVG4ZDMMBUGE__;!!Mih3wA!AAWj8yKpP6mmsoDF-8Taol8M6UzfrJW4ld8Vv9siiYq50VqAQildtkdg3_KcQf15dmwCgA-o6itbdhB7gHrRx8Py$ . You are receiving this because you commented.Message ID: @.***>
--
I would expect
cabal exec ghc -- -plugin=LiquidHaskell Test.hs
to output .liquid
in the current working directory (./.liquid
), and
cabal exec ghc -- -hidir=output-folder -plugin=LiquidHaskell Test.hs
to output in ./output-folder/.liquid
, -hidir being a ghc
flag.
If building a package
cabal build liquid-prelude
would place files in
dist-newstyle/build/x86_64-linux/ghc-9.8.1/liquid-prelude-0.9.2.8.1/build/Language/Haskell/Liquid/.liquid
dist-newstyle/build/x86_64-linux/ghc-9.8.1/liquid-prelude-0.9.2.8.1/build/Language/Haskell/Liquid/RTick/.liquid
and
stack build liquid-prelude
would place them in
liquid-prelude/.stack-work/dist/x86_64-linux-nix/ghc-9.8.1/build/Language/Haskell/Liquid/.liquid
liquid-prelude/.stack-work/dist/x86_64-linux-nix/ghc-9.8.1/build/Language/Haskell/Liquid/RTick/.liquid
Currently, running liquidhaskell as GHC plugin fills my source directory with
.liquid
sub-directories. Can we have these directories indist
/dist-newstyle
instead?