Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Haskabelle problems

Email Gateway (Aug 19 2022 at 08:59):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

I'm struggling a bit with Haskabelle at the moment. I think I set it up
correctly, it compiled and everything, but as soon as I try to use it on
a simple file - say, something like this…

Test.hs:

module Test where

itrev [] xs = xs
itrev (x:xs) ys = itrev xs (x:ys)

…with a command like this…

isabelle haskabelle Test.hs thy/

…I get the following error message:

Warning: File or directory "Test.hs" does not exist!haskabelle_bin:
user error (Internal error: No Haskell module was parsed!)
Even though the file most definitely exists.

So I tried using the entire directory as the source:

isabelle haskabelle ./ thy/

But:

haskabelle_bin: user error (The module "Data.Maybe" imported from
module "Importer.Hsx" cannot be found at "./Data/Maybe.hs"!)
On another system, with the same setup, I get:
haskabelle_bin: user error (The module "Data.List" imported from
module "Importer.Library" cannot be found at "./Data/List.hs"!)

GHC works fine and Test.hs compiles without problems, so all the
required modules seem to be there. In fact, isabelle haskabelle -e (i.e.
running the examples through Haskabelle) also seems to work. What am I
doing wrong?

Cheers
Manuel

Email Gateway (Aug 19 2022 at 09:16):

From: Lars Noschinski <noschinl@in.tum.de>
On 15.10.2012 02:18, Manuel Eberl wrote:

I'm struggling a bit with Haskabelle at the moment. I think I set it up
correctly, it compiled and everything, but as soon as I try to use it on
a simple file - say, something like this…
[...]

…I get the following error message:

Warning: File or directory "Test.hs" does not exist!haskabelle_bin:
user error (Internal error: No Haskell module was parsed!)
Even though the file most definitely exists.

There is a bug in the haskabelle run script which changes the current
working directory and therefore breaks relative paths. I have fixed it
now in the repository.

So I tried using the entire directory as the source:

isabelle haskabelle ./ thy/

So with this bug, ./ refers to the Haskabelle directory ...

But:

haskabelle_bin: user error (The module "Data.Maybe" imported from
module "Importer.Hsx" cannot be found at "./Data/Maybe.hs"!)
On another system, with the same setup, I get:
haskabelle_bin: user error (The module "Data.List" imported from
module "Importer.Library" cannot be found at "./Data/List.hs"!)

... and tries to import Haskabelle itself.

-- Lars

Last updated: Apr 26 2024 at 08:19 UTC