Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] isabelle ghc_setup

Email Gateway (Apr 13 2021 at 16:15):

From: Peter Lammich <lammich@in.tum.de>
Hi List,

the isabelle ghc_setup seems to magically setup Haskell using stack,
such that I can run, e.g., export_code checking Haskell. However, I
cannot find any documentation on this. Is there any?

Question: How can I install additional packages from hackage?

I use some code_printing setup with additional packages, but find no
way how "export_code checking" would find them:

export_code test checking Haskell

Heap.hs:8:1: error:
Could not find module ‘Control.Monad.Parallel’
Perhaps you meant
Control.Monad.Fail (from base-4.13.0.0)
Control.Monad.Reader (from mtl-2.2.2)
Control.Monad.State (from mtl-2.2.2)
Use -v (or :set -v in ghci) to see a list of the files searched
for.
|
8 | import Control.Monad.Parallel(bindM2)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Email Gateway (May 16 2021 at 14:18):

From: Makarius <makarius@sketis.net>
On 13/04/2021 18:15, Peter Lammich wrote:

the isabelle ghc_setup seems to magically setup Haskell using stack,
such that I can run, e.g., export_code checking Haskell. However, I
cannot find any documentation on this. Is there any?

There is not much going on in "isabelle ghc_setup": it merely delegates
everything to regular "stack" with some options provided via Isabelle settings:

https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/lib/scripts/getfunctions#l46

So the main documentation is https://docs.haskellstack.org

Question: How can I install additional packages from hackage?

Packages for "stack" come from "stackage" instead of "hackage".

You probably need a Haskell stack project to use packages. Here is a small
example:

https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/src/Tools/Haskell/Test.thy#l11

https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/src/Pure/Tools/ghc.ML#l49

I use some code_printing setup with additional packages, but find no
way how "export_code checking" would find them:

export_code test checking Haskell

Heap.hs:8:1: error:
Could not find module ‘Control.Monad.Parallel’
Perhaps you meant
Control.Monad.Fail (from base-4.13.0.0)
Control.Monad.Reader (from mtl-2.2.2)
Control.Monad.State (from mtl-2.2.2)
Use -v (or :set -v in ghci) to see a list of the files searched
for.
|
8 | import Control.Monad.Parallel(bindM2)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I can't say anything about "export_code ... checking Haskell".

Makarius

Last updated: Jan 04 2025 at 20:18 UTC