Skip to content
Snippets Groups Projects
Unverified Commit 4b924bb4 authored by Rodrigo Mesquita's avatar Rodrigo Mesquita :seedling:
Browse files

Migrate v3 Agda

parent f410478d
No related branches found
No related tags found
1 merge request!23Wip/romes/migration v2 + v3
Pipeline #93009 failed
diff --git a/Agda.cabal b/Agda.cabal
index 306f81f..5aa17c3 100644
index 306f81f..0082221 100644
--- a/Agda.cabal
+++ b/Agda.cabal
@@ -1,7 +1,7 @@
@@ -1,8 +1,8 @@
+cabal-version: 3.12
name: Agda
version: 2.6.3
cabal-version: 1.24
-cabal-version: 1.24
-build-type: Custom
-license: OtherLicense
+build-type: Hooks
license: OtherLicense
+-- license: OtherLicense
license-file: LICENSE
copyright: (c) 2005-2023 The Agda Team.
@@ -172,7 +172,7 @@ flag optimise-heavily
author: Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html
@@ -172,7 +172,8 @@ flag optimise-heavily
custom-setup
setup-depends: base >= 4.9.0.0 && < 4.18
- , Cabal >= 1.24.0.0 && < 3.9
+ , Cabal >= 1.24.0.0 && < 3.12
+ , Cabal-hooks
, directory >= 1.2.6.2 && < 1.4
, filepath >= 1.4.1.0 && < 1.5
, process >= 1.4.2.0 && < 1.7
@@ -184,7 +185,7 @@ library
-- We don't write an upper bound for cpphs because the
-- `build-tools` field can not be modified in Hackage.
- build-tools: cpphs >= 1.20.9
+ build-tool-depends: cpphs:cpphs >= 1.20.9
ghc-options: -pgmP cpphs -optP --cpp
if flag(debug)
@@ -280,8 +281,9 @@ library
-- We don't write upper bounds for Alex nor Happy because the
-- `build-tools` field can not be modified in Hackage. Agda doesn't
-- build with Alex 3.2.0 and segfaults with 3.2.2.
- build-tools: alex >= 3.1.0 && < 3.2.0 || == 3.2.1 || >= 3.2.3
- , happy >= 1.19.4
+ build-tool-depends:
+ alex:alex >= 3.1.0 && < 3.2.0 || == 3.2.1 || >= 3.2.3,
+ happy:happy >= 1.19.4
exposed-modules: Agda.Auto.Auto
Agda.Auto.Options
diff --git a/Setup.hs b/SetupHooks.hs
similarity index 53%
similarity index 52%
rename from Setup.hs
rename to SetupHooks.hs
index 3a42cd2..0877357 100644
index 3a42cd2..fff18d0 100644
--- a/Setup.hs
+++ b/SetupHooks.hs
@@ -1,16 +1,20 @@
@@ -1,16 +1,21 @@
-{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
+{-# LANGUAGE OverloadedStrings #-}
......@@ -37,6 +62,7 @@ index 3a42cd2..0877357 100644
import Data.Maybe
+import Distribution.Utils.Path (getSymbolicPath, makeSymbolicPath, makeRelativePathEx)
import Distribution.Simple
import Distribution.Simple.LocalBuildInfo
+import Distribution.Simple.Install (installFileGlob)
......@@ -51,7 +77,7 @@ index 3a42cd2..0877357 100644
import System.FilePath
import System.Directory (makeAbsolute, removeFile)
import System.Environment (getEnvironment)
@@ -19,58 +23,52 @@ import System.Exit
@@ -19,58 +24,53 @@ import System.Exit
import System.IO
import System.IO.Error (isDoesNotExistError)
......@@ -141,19 +167,20 @@ index 3a42cd2..0877357 100644
+copyInterfaceFiles :: LocalBuildInfo -> CopyFlags -> IO ()
+copyInterfaceFiles lbi flags = do
+ let pd = localPkgDescr lbi
+ src = dataDir pd
+ src = getSymbolicPath $ dataDir pd
+ dst = datadir $ absoluteInstallDirs pd lbi ( fromFlag $ copyDest flags )
+ for_ ( dataFiles pd ) $ \ fp ->
+ for_ ( getSymbolicPath <$> dataFiles pd ) $ \ fp ->
+ when ( takeExtension fp == ".agda" ) $
+ installFileGlob
+ ( fromFlag $ copyVerbosity flags )
+ ( specVersion pd )
+ ( src, dst )
+ ( toIFile fp )
+ Nothing
+ ( Just $ makeSymbolicPath src, makeSymbolicPath dst )
+ ( makeRelativePathEx $ toIFile fp )
toIFile :: FilePath -> FilePath
toIFile file = replaceExtension file ".agdai"
@@ -80,15 +78,16 @@ toIFile file = replaceExtension file ".agdai"
@@ -80,15 +80,16 @@ toIFile file = replaceExtension file ".agdai"
skipInterfaces :: LocalBuildInfo -> Bool
skipInterfaces lbi = fromPathTemplate (progSuffix lbi) == "-quicker"
......@@ -169,12 +196,16 @@ index 3a42cd2..0877357 100644
-- then...
- let bdir = buildDir lbi
+ let pd = localPkgDescr lbi
+ bdir = buildDir lbi
+ bdir = getSymbolicPath $ buildDir lbi
agda = bdir </> "agda" </> "agda" <.> agdaExeExtension
ddir <- makeAbsolute $ "src" </> "data"
@@ -102,7 +101,7 @@ generateInterfaces pd lbi = do
let builtins = filter ((== ".agda") . takeExtension) (dataFiles pd)
@@ -99,10 +100,10 @@ generateInterfaces pd lbi = do
putStrLn "Generating Agda library interface files..."
-- The Agda.Primitive* and Agda.Builtin* modules.
- let builtins = filter ((== ".agda") . takeExtension) (dataFiles pd)
+ let builtins = filter ((== ".agda") . takeExtension) (getSymbolicPath <$> dataFiles pd)
-- Remove all existing .agdai files.
- forM_ builtins $ \fp -> do
......@@ -182,7 +213,7 @@ index 3a42cd2..0877357 100644
let fullpathi = toIFile (ddir </> fp)
handleExists e | isDoesNotExistError e = return ()
@@ -140,8 +139,4 @@ generateInterfaces pd lbi = do
@@ -140,8 +141,4 @@ generateInterfaces pd lbi = do
return ()
agdaExeExtension :: String
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment