Re: [isabelle] Haskabelle and Literate Haskell



Hi Artur,

> I'm planning to use haskabelle in my research and currently
> I'm using literate Haskell.
> However, as far as I could go, I noticed that Haskabelle
> searches for *.hs files, plain haskell.
> 
> Is there something I could do in order to use my Literate Haskell files,
> or it is mandatory to use plain haskell for it?

I am not sure whether I understand your question correctly.

Using Haskabelle from the Isabelle2016 release:

> Usage: isabelle haskabelle [OPTIONS] [SRC... DST]
> 
>   Options are:
>     SRC...     list of haskell source files
>     DST        destination directory
>     -a DIR     custom adaptation table (default /home/haftmann/.isabelle/Isabelle2016/Haskabelle-2015/default)
>     -c CONFIG  configuration file
>     -e         runs the Haskabelle examples
>     -r         rebuild adaptation table
>     -v         show Haskabelle version

Which seems to suggest to you just specify the source files regardless
of any file extension.  Whether Literate Haskell files will work depends
on whether the underlying parser library handles this gracefully, which
I don't know.  If not, the simplest solution might be a separate
preprocessor to extract Haskell source from Literate Haskell source and
giving that result to Haskabelle.  See ghc --help for hints on that.

Hope this helps,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.