Feature request: prepend {-# OPTIONS_GHC -w #-} to extracted Haskell files

[toku-sa-n]

Is your feature request related to a problem?

When I try compiling an extracted Haskell file with -Weverything, GHC complains about many things against the file.

Proposed solution

Prepend {-# OPTIONS_GHC -w #-} to disable all warnings when extracting Haskell files.

Alternative solutions

Fix every warning and error after the extraction. This is very troublesome.

Additional context

Although the use of -Weverything is very extreme, I believe disabling all warnings and errors is reasonable. One example is that Cabal, an official Haskell build tool, generates Paths_*.hs with the pragma.

[JasonGross]

There is Set Extraction File Comment, but it does not work for this purpose.

From Coq Require Import Extraction.

Extraction Language Haskell.
Set Extraction File Comment "{-# OPTIONS_GHC -w #-}".
Recursive Extraction id.

gives

{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

{- {-# OPTIONS_GHC -w #-} -}

module Main where

import qualified Prelude

#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#if __GLASGOW_HASKELL__ >= 900
import qualified GHC.Exts
#endif
#else
-- HUGS
import qualified IOExts
#endif

#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif

id :: Any -> Any
id x =
  x

I propose that if the extraction file comment begins with {-#, then the magic header should be disabled in Haskell.