[ pkgs ] Add package system to Agda.

.gitignore

@@ -25,7 +25,8 @@ dist-*/
 Epic
 examples/compiler/main
 hlint-report.html
-MAlonzo
+**/MAlonzo/*
+!src/data/MAlonzo-RTE/**/*.hs
 mk/config.mk
 notes/style/haskell-style.tex
 src/full/Agda/Syntax/Parser/Lexer.hs

Agda.cabal

@@ -47,10 +47,16 @@ data-files:         Agda.css
                     agda.sty
                     postprocess-latex.pl
                     lib/prim/Agda/Primitive.agda
+                    lib/agda-pkg.yaml
                     uhc-agda-base/LICENSE
                     uhc-agda-base/uhc-agda-base.cabal
                     uhc-agda-base/src/UHC/Agda/*.hs
-                    MAlonzo/src/MAlonzo/*.hs
+                    MAlonzo-RTE/src/MAlonzo/*.hs
+                    MAlonzo-RTE/Agda-MAlonzo-RTE.cabal
+                    MAlonzo-RTE/Setup.hs
+                    MAlonzo-RTE/LICENSE
+                    fauchi/config
+                    fauchi/stack.yaml
 
 source-repository head
   type:     git
@@ -85,7 +91,8 @@ library
     build-depends:  Win32 >= 2.2 && < 2.4
 
   build-depends:
-    array >= 0.4.0.1 && < 0.6
+      aeson >= 0.9.0.0 && < 1.1
+    , array >= 0.4.0.1 && < 0.6
     , base >= 4.6.0.1 && < 4.10
     , binary >= 0.7.2.1 && < 0.9
     , boxes >= 0.1.3 && < 0.2
@@ -240,6 +247,9 @@ library
                     Agda.Interaction.Options
                     Agda.Interaction.Options.Lenses
                     Agda.Main
+                    Agda.Packaging.Base
+                    Agda.Packaging.Config
+                    Agda.Packaging.Database
                     Agda.Syntax.Abstract.Copatterns
                     Agda.Syntax.Abstract.Name
                     Agda.Syntax.Abstract.Pretty
@@ -554,6 +564,63 @@ executable agda-ghc-names
     , filepath >= 1.3.0.1 && < 1.5
   ghc-options:  -rtsopts
 
+executable fauchi
+  hs-source-dirs:   src/fauchi
+  main-is:          Main.hs
+  build-depends:    Agda == 2.5
+                  , aeson >= 0.9.0.0 && < 1.1
+                  , base >= 4.6.0.1 && < 6
+                  , bytestring >= 0.10.0.2 && < 0.11
+                  , containers >= 0.5.0.0 && < 0.6
+                  , directory >= 1.2.0.1 && < 1.3
+                  , exceptions >= 0.8.0.2 && < 0.9
+                  , filepath >= 1.3.0.1 && < 1.5
+                    -- mtl-2.1 contains a severe bug.
+                    --
+                    -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.
+                  , mtl >= 2.1.1 && <= 2.1.3.1 || >= 2.2.1 && < 2.3
+                  , optparse-applicative >= 0.11.0.2 && < 13
+                  , process >= 1.1.0.2 && < 1.3
+                  , process-extras >= 0.3.0 && < 0.4
+                  , text >= 0.11.3.1 && < 1.3
+                  , yaml >= 0.8.15.2 && < 0.9
+  other-modules:    Fauchi.Build
+                  , Fauchi.Error
+                  , Fauchi.Internal
+                  , Fauchi.Monad
+                  , Fauchi.PackageDesc
+                  , Fauchi.PackageDesc.Base
+
+  if impl(ghc >= 7.6.3)
+    ghc-options: -w
+                 -Werror
+                 -fwarn-deprecated-flags
+                 -fwarn-dodgy-exports
+                 -fwarn-dodgy-foreign-imports
+                 -fwarn-dodgy-imports
+                 -fwarn-duplicate-exports
+                 -fwarn-hi-shadowing
+                 -fwarn-identities
+                 -fwarn-incomplete-patterns
+                 -fwarn-missing-fields
+                 -fwarn-missing-methods
+                 -fwarn-missing-signatures
+                 -fwarn-monomorphism-restriction
+                 -fwarn-orphans
+                 -fwarn-pointless-pragmas
+                 -fwarn-tabs
+                 -fwarn-overlapping-patterns
+                 -fwarn-unrecognised-pragmas
+                 -fwarn-unused-do-bind
+                 -fwarn-warnings-deprecations
+                 -fwarn-wrong-do-bind
+
+  if impl(ghc >= 7.8)
+    ghc-options: -fwarn-duplicate-constraints
+                 -fwarn-empty-enumerations
+                 -fwarn-overflowed-literals
+                 -fwarn-typed-holes
+                 -fwarn-inline-rule-shadowing
 
 -- Cabal testsuite integration has some serious bugs, but we
 -- can still make it work. See also:

LICENSE

@@ -5,7 +5,7 @@ Alan Jeffrey, Makoto Takeyama, Andrea Vezzosi, Nicolas Pouillard,
 James Chapman, Jean-Philippe Bernardy, Fredrik Lindblad, Nobuo
 Yamashita, Fredrik Nordvall Forsberg, Patrik Jansson, Guilhem Moulin,
 Stefan Monnier, Marcin Benke, Olle Fredriksson, Darin Morrison, Jesper
-Cockx, Wolfram Kahl, Catarina Coquand
+Cockx, Wolfram Kahl, Catarina Coquand, Philipp Hausmann
 
 Permission is hereby granted, free of charge, to any person obtaining
 a copy of this software and associated documentation files (the

Setup.hs

@@ -7,19 +7,50 @@ import Distribution.PackageDescription
 import System.FilePath
 import System.Process
 import System.Exit
+import System.Directory
+import Data.Version
+import Control.Exception
+import Data.List
 
 main = defaultMainWithHooks hooks
 
-hooks = simpleUserHooks { postInst = checkAgdaPrimitive }
+hooks = simpleUserHooks {- postInst = checkAgdaPrimitive,-} { postCopy = checkAgdaPrimitive }
 
-checkAgdaPrimitive :: Args -> InstallFlags -> PackageDescription -> LocalBuildInfo -> IO ()
+checkAgdaPrimitive :: Args -> a -> PackageDescription -> LocalBuildInfo -> IO ()
 checkAgdaPrimitive args flags pkg info = do
   let dirs = absoluteInstallDirs pkg info NoCopyDest
       agda = buildDir info </> "agda" </> "agda" <.> exeExtension
-      prim = datadir dirs </> "lib" </> "prim" </> "Agda" </> "Primitive" <.> "agda"
-  putStrLn "Generating Agda library interface files..."
-  ok <- rawSystem agda [prim, "-v0"]
-  case ok of
+      prim = datadir dirs </> "lib"
+      version = pkgVersion $ package pkg
+      pkgDir = datadir dirs </> showVersion version </> "packages"
+      mazRTEDir = datadir dirs </> "MAlonzo-RTE"
+
+  fauchi <- makeAbsolute $ buildDir info </> "fauchi" </> "fauchi" <.> exeExtension
+
+  pkgDirExists <- doesDirectoryExist pkgDir
+  if pkgDirExists
+    then do
+      putStrLn $ "Removing old Agda package db (" ++ pkgDir ++ ") ..."
+      removeDirectoryRecursive pkgDir
+    else return ()
+
+  putStrLn $ "Setting up Agda default package DB ..."
+  putStrLn $ "Using fauchi: " ++ fauchi
+
+  callProcess fauchi ["init-pkg-db", pkgDir]
+
+  putStrLn "Installing Agda-Primitives package ..."
+
+  callProcess fauchi ["install-primitives", "--disable-ghc-binaries", "--agda-package-db=${GLOBAL_DB}"]
+
+
+callProcess' :: FilePath -> FilePath -> [String] -> IO ()
+callProcess' wd exe args = do
+  (_, _, _, p) <- createProcess $ (proc exe args) { cwd = Just wd }
+  r <- waitForProcess p
+  case r of
     ExitSuccess   -> return ()
-    ExitFailure _ -> putStrLn "WARNING: Failed to typecheck Agda.Primitive!"
+    ExitFailure _ -> do
+      putStrLn "WARNING: Failed to typecheck Agda.Primitive!"
+      exitWith $ ExitFailure (-1)
 

default.nix

@@ -21,15 +21,15 @@
 # To enter the development environment, simply call `nix-shell shell.nix`.
 #
 
-{ mkDerivation, alex, array, base, binary, boxes, bytestring
+{ mkDerivation, alex, aeson, array, base, binary, boxes, bytestring
 , containers, cpphs, data-hash, deepseq, directory, edit-distance
 , emacs, equivalence, filepath, geniplate-mirror, happy, hashable
 , hashtables, haskeline, haskell-src-exts, mtl, parallel, pretty
 , process, process-extras, QuickCheck, stdenv, strict, tasty
 , regex-tdfa, regex-tdfa-text, filemanip
 , tasty-silver, template-haskell, temporary, text, time
 , transformers, transformers-compat, unordered-containers, xhtml
-, zlib, tasty-quickcheck, monadplus, EdisonCore, EdisonAPI
+, zlib, tasty-quickcheck, monadplus, EdisonCore, EdisonAPI, optparse-applicative, yaml, exceptions
 , uhc-backend ? false, uhc ? null, uhc-light ? null
 , user-manual ? true, sphinx ? null, sphinx_rtd_theme ? null, texLive ? null
 }:
@@ -44,12 +44,12 @@ mkDerivation {
   isLibrary = true;
   isExecutable = true;
   buildDepends = [
-    array base binary boxes bytestring containers data-hash deepseq
+    aeson array base binary boxes bytestring containers data-hash deepseq
     directory edit-distance equivalence filepath geniplate-mirror
     hashable hashtables haskeline haskell-src-exts mtl parallel pretty
     process QuickCheck strict template-haskell text time transformers filemanip
     transformers-compat unordered-containers xhtml zlib uhc-light tasty-quickcheck
-    monadplus EdisonCore EdisonAPI
+    monadplus EdisonCore EdisonAPI optparse-applicative yaml exceptions
   ];
   testDepends = [
     base containers directory filepath process-extras tasty

src/data/MAlonzo-RTE/Agda-MAlonzo-RTE.cabal

@@ -0,0 +1,25 @@
+-- Initial Agda-MAlonzo-RTE.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                Agda-MAlonzo-RTE
+version:             $$AGDA_VERSION$$
+synopsis:            Runtime support for the Agda MAlonzo compiler.
+-- description:         
+homepage:            http://wiki.portal.chalmers.se/agda/
+-- license:             
+license-file:        LICENSE
+author:              The Agda Team (see Agda package)
+maintainer:          Philipp Hausmann <ph_git@314.ch>
+-- copyright:           
+category:            Dependent types
+build-type:          Simple
+-- extra-source-files:  
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     MAlonzo.RTE
+  -- other-modules:       
+  -- other-extensions:    
+  build-depends:       base >=4.8 && <4.9, ghc-prim >=0.4 && <0.5
+  hs-source-dirs:      src
+  default-language:    Haskell2010

src/data/MAlonzo-RTE/LICENSE

@@ -0,0 +1,28 @@
+Copyright (c) 2005-2015 Ulf Norell, Andreas Abel, Nils Anders
+Danielsson, Andrés Sicard-Ramírez, Dominique Devriese, Péter
+Divianszki, Francesco Mazzoli, Stevan Andjelkovic, Daniel Gustafsson,
+Alan Jeffrey, Makoto Takeyama, Andrea Vezzosi, Nicolas Pouillard,
+James Chapman, Jean-Philippe Bernardy, Fredrik Lindblad, Nobuo
+Yamashita, Fredrik Nordvall Forsberg, Patrik Jansson, Guilhem Moulin,
+Stefan Monnier, Marcin Benke, Olle Fredriksson, Darin Morrison, Jesper
+Cockx, Wolfram Kahl, Catarina Coquand, Philipp Hausmann
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+

src/data/MAlonzo-RTE/Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain