mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
commit
53f6fc98b1
57
.travis.yml
57
.travis.yml
@ -1,5 +1,4 @@
|
||||
dist: trusty
|
||||
sudo: false
|
||||
dist: xenial
|
||||
|
||||
language: c
|
||||
|
||||
@ -11,33 +10,25 @@ matrix:
|
||||
include:
|
||||
- env: CABALVER="2.4" GHCVER="8.6.5" STACKVER="14.15" STYLISH=YES
|
||||
addons: {apt: {packages: [cabal-install-2.4,ghc-8.6.5,hscolour], sources: [hvr-ghc]}}
|
||||
- env: CABALVER="2.2" GHCVER="7.10.3" TESTS="test_c"
|
||||
compiler: ": #GHC 7.10.3"
|
||||
addons: {apt: {packages: [cabal-install-2.2,ghc-7.10.3,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
# Disabled because it's always timing out
|
||||
# - env: CABALVER="1.24" GHCVER="8.0.1" TESTS="test_c"
|
||||
# compiler: ": #GHC 8.0.1"
|
||||
# addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.1,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
- env: CABALVER="2.0" GHCVER="8.2.2" TESTS="lib_doc doc"
|
||||
- env: CABALVER="2.4" GHCVER="8.2.2" TESTS="lib_doc doc"
|
||||
compiler: ": #GHC 8.2.2"
|
||||
addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
- env: CABALVER="2.0" GHCVER="8.2.2" TESTS="test_js"
|
||||
addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
- env: CABALVER="2.4" GHCVER="8.2.2" TESTS="test_js"
|
||||
compiler: ": #GHC 8.2.2"
|
||||
addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
- env: CABALVER="2.0" GHCVER="8.2.2" TESTS="test_c"
|
||||
addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
- env: CABALVER="2.4" GHCVER="8.2.2" TESTS="test_c"
|
||||
compiler: ": #GHC 8.2.2"
|
||||
addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
#TODO: The idris built with those fails due to libffi dynamic linking version mismatch.
|
||||
# Caused by the GHC backport to Trusty?
|
||||
# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="lib_doc doc"
|
||||
# compiler: ": #GHC 8.4.1"
|
||||
# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="test_js"
|
||||
# compiler: ": #GHC 8.4.1"
|
||||
# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
# - env: CABALVER="2.2" GHCVER="8.4.1" TESTS="test_c"
|
||||
# compiler: ": #GHC 8.4.1"
|
||||
# addons: {apt: {packages: [cabal-install-2.2,ghc-8.4.1,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
addons: {apt: {packages: [cabal-install-2.4,ghc-8.2.2,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
|
||||
# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="lib_doc doc"
|
||||
# compiler: ": #GHC 8.8.1"
|
||||
# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="test_js"
|
||||
# compiler: ": #GHC 8.8.1"
|
||||
# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
# - env: CABALVER="3.0" GHCVER="8.8.1" TESTS="test_c"
|
||||
# compiler: ": #GHC 8.8.1"
|
||||
# addons: {apt: {packages: [cabal-install-3.0,ghc-8.8.1,cppcheck,hscolour], sources: [hvr-ghc]}}
|
||||
fast-finish: true
|
||||
|
||||
cache:
|
||||
@ -88,7 +79,7 @@ install:
|
||||
# causing cabal's default configuration (jobs: $ncpus)
|
||||
# to run into the GHC #9221 bug which can result in longer build-times.
|
||||
- $SED -i -r 's/(^jobs:).*/\1 2/' $HOME/.cabal/config
|
||||
- cabal install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt
|
||||
- cabal v1-install -f FFI --only-dependencies --enable-tests --dry -v > installplan.txt
|
||||
- $SED -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
|
||||
# check whether current requested install-plan matches cached package-db snapshot
|
||||
- if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;
|
||||
@ -101,7 +92,7 @@ install:
|
||||
echo "cabal build-cache MISS";
|
||||
rm -rf $HOME/.cabsnap;
|
||||
mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
|
||||
cabal install -f FFI --only-dependencies --enable-tests;
|
||||
cabal v1-install -f FFI --only-dependencies --enable-tests;
|
||||
fi
|
||||
# snapshot package-db on cache miss
|
||||
- if [ ! -d $HOME/.cabsnap ];
|
||||
@ -114,26 +105,26 @@ install:
|
||||
|
||||
before_script:
|
||||
- ORIGINAL_DIR=$(pwd)
|
||||
- cabal sdist
|
||||
- cabal v1-sdist
|
||||
- cd ..
|
||||
- tar -xf ${ORIGINAL_DIR}/dist/${PKGNAME}*.tar.gz
|
||||
- cd ${PKGNAME}*
|
||||
script:
|
||||
###
|
||||
- echo 'Configure...' && echo -en 'travis_fold:start:script.configure\\r'
|
||||
- cabal configure -f FFI -f CI --enable-tests
|
||||
- cabal v1-configure -f FFI -f CI --enable-tests
|
||||
- echo -en 'travis_fold:end:script.configure\\r'
|
||||
###
|
||||
- echo 'Build...' && echo -en 'travis_fold:start:script.build\\r'
|
||||
- cabal build
|
||||
- cabal v1-build
|
||||
- echo -en 'travis_fold:end:script.build\\r'
|
||||
###
|
||||
- echo 'Copy...' && echo -en 'travis_fold:start:script.copy\\r'
|
||||
- cabal copy
|
||||
- cabal v1-copy
|
||||
- echo -en 'travis_fold:end:script.copy\\r'
|
||||
###
|
||||
- echo 'Register...' && echo -en 'travis_fold:start:script.register\\r'
|
||||
- cabal register
|
||||
- cabal v1-register
|
||||
- echo -en 'travis_fold:end:script.register\\r'
|
||||
###
|
||||
- echo 'Cppcheck...' && echo -en 'travis_fold:start:script.cppcheck\\r'
|
||||
|
@ -1,3 +1,6 @@
|
||||
# New since last release
|
||||
+ Updated to work with GHC 8.8 and cabal 3.0
|
||||
|
||||
# New in 1.3.2
|
||||
+ Documentation added to proof section
|
||||
|
||||
|
8
Makefile
8
Makefile
@ -30,15 +30,15 @@ stylize:
|
||||
./stylize.sh
|
||||
|
||||
test_c:
|
||||
$(CABAL) test $(ARGS) --test-options \
|
||||
$(CABAL) v1-test $(ARGS) --test-options \
|
||||
"$(TEST-ARGS) --rerun-update +RTS -N$(TEST-JOBS) -RTS"
|
||||
|
||||
test_js:
|
||||
$(CABAL) test $(ARGS) --test-options \
|
||||
$(CABAL) v1-test $(ARGS) --test-options \
|
||||
"$(TEST-ARGS) --node --rerun-update +RTS -N$(TEST-JOBS) -RTS"
|
||||
|
||||
test_update:
|
||||
$(CABAL) test $(ARGS) --test-options \
|
||||
$(CABAL) v1-test $(ARGS) --test-options \
|
||||
"$(TEST-ARGS) --accept +RTS -N$(TEST-JOBS) -RTS"
|
||||
|
||||
test_clean:
|
||||
@ -56,7 +56,7 @@ linecount:
|
||||
|
||||
#Note: this doesn't yet link to Hackage properly
|
||||
doc: dist/setup-config
|
||||
$(CABAL) haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
|
||||
$(CABAL) v1-haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
|
||||
|
||||
lib_doc:
|
||||
$(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc
|
||||
|
33
Setup.hs
33
Setup.hs
@ -215,36 +215,6 @@ idrisConfigure _ flags pkgdesc local = do
|
||||
autogenComponentModulesDir lbi _ = autogenModulesDir lbi
|
||||
#endif
|
||||
|
||||
idrisPreSDist args flags = do
|
||||
let dir = S.fromFlag (S.sDistDirectory flags)
|
||||
let verb = S.fromFlag (S.sDistVerbosity flags)
|
||||
generateVersionModule verb "src" True
|
||||
generateBuildFlagsModule verb "src" []
|
||||
generateTargetModule verb "src" "./libs"
|
||||
generateToolchainModule verb "src" Nothing
|
||||
preSDist simpleUserHooks args flags
|
||||
|
||||
idrisSDist sdist pkgDesc bi hooks flags = do
|
||||
pkgDesc' <- addGitFiles pkgDesc
|
||||
sdist pkgDesc' bi hooks flags
|
||||
where
|
||||
addGitFiles :: PackageDescription -> IO PackageDescription
|
||||
addGitFiles pkgDesc = do
|
||||
files <- gitFiles
|
||||
return $ pkgDesc { extraSrcFiles = extraSrcFiles pkgDesc ++ files}
|
||||
gitFiles :: IO [FilePath]
|
||||
gitFiles = liftM lines (readProcess "git" ["ls-files"] "")
|
||||
|
||||
idrisPostSDist args flags desc lbi = do
|
||||
Control.Exception.catch (do let file = "src" </> "Version_idris" Px.<.> "hs"
|
||||
let targetFile = "src" </> "Target_idris" Px.<.> "hs"
|
||||
putStrLn $ "Removing generated modules:\n "
|
||||
++ file ++ "\n" ++ targetFile
|
||||
removeFile file
|
||||
removeFile targetFile)
|
||||
(\e -> let e' = (e :: SomeException) in return ())
|
||||
postSDist simpleUserHooks args flags desc lbi
|
||||
|
||||
#if !(MIN_VERSION_Cabal(2,0,0))
|
||||
rewriteFileEx :: Verbosity -> FilePath -> String -> IO ()
|
||||
rewriteFileEx _ = rewriteFile
|
||||
@ -353,8 +323,5 @@ main = defaultMainWithHooks $ simpleUserHooks
|
||||
, postInst = \_ flags pkg local ->
|
||||
idrisInstall (S.fromFlag $ S.installVerbosity flags)
|
||||
NoCopyDest pkg local
|
||||
, preSDist = idrisPreSDist
|
||||
, sDistHook = idrisSDist (sDistHook simpleUserHooks)
|
||||
, postSDist = idrisPostSDist
|
||||
, testHook = idrisTestHook
|
||||
}
|
||||
|
@ -1,17 +1,17 @@
|
||||
version: 1.0.{build}
|
||||
init:
|
||||
- ps: >-
|
||||
choco install cabal --version=2.4.1.0 --no-progress
|
||||
choco install cabal --no-progress
|
||||
|
||||
mkdir C:\ghc
|
||||
|
||||
Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
|
||||
Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.8.2/ghc-8.8.2-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
|
||||
|
||||
7z x C:\ghc\ghc.tar.xz -oC:\ghc
|
||||
|
||||
7z x C:\ghc\ghc.tar -oC:\ghc
|
||||
|
||||
$env:PATH="$env:PATH;c:\ghc\ghc-8.4.3\bin;$HOME\AppData\Roaming\cabal\bin"
|
||||
$env:PATH="$env:PATH;c:\ghc\ghc-8.8.2\bin;$HOME\AppData\Roaming\cabal\bin"
|
||||
|
||||
cabal v1-update
|
||||
|
||||
|
128
idris.cabal
128
idris.cabal
@ -1,6 +1,7 @@
|
||||
Cabal-Version: 2.4
|
||||
Name: idris
|
||||
Version: 1.3.2
|
||||
License: BSD3
|
||||
License: BSD-3-Clause
|
||||
License-file: LICENSE
|
||||
Author: Edwin Brady
|
||||
Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
|
||||
@ -41,42 +42,18 @@ Description: Idris is a general purpose language with full dependent types.
|
||||
.
|
||||
* Hugs style interactive environment
|
||||
|
||||
Cabal-Version: >= 1.22
|
||||
|
||||
Build-type: Custom
|
||||
|
||||
Tested-With: GHC == 7.10.3, GHC == 8.0.1
|
||||
|
||||
Data-files: idrisdoc/styles.css
|
||||
jsrts/jsbn/jsbn-browser.js
|
||||
jsrts/jsbn/jsbn-node.js
|
||||
jsrts/Runtime-common.js
|
||||
jsrts/Runtime-javascript.js
|
||||
jsrts/Runtime-node.js
|
||||
jsrts/**/*.js
|
||||
jsrts/jsbn/LICENSE
|
||||
rts/arduino/idris_main.c
|
||||
rts/idris_bitstring.c
|
||||
rts/idris_bitstring.h
|
||||
rts/idris_gc.c
|
||||
rts/idris_gc.h
|
||||
rts/idris_gmp.c
|
||||
rts/idris_gmp.h
|
||||
rts/idris_heap.c
|
||||
rts/idris_heap.h
|
||||
rts/idris_main.c
|
||||
rts/idris_net.c
|
||||
rts/idris_net.h
|
||||
rts/idris_opts.c
|
||||
rts/idris_opts.h
|
||||
rts/idris_rts.c
|
||||
rts/idris_rts.h
|
||||
rts/idris_stats.c
|
||||
rts/idris_stats.h
|
||||
rts/idris_stdfgn.c
|
||||
rts/idris_stdfgn.h
|
||||
rts/mini-gmp.c
|
||||
rts/mini-gmp.h
|
||||
rts/libtest.c
|
||||
rts/Makefile
|
||||
rts/**/*.c
|
||||
rts/**/*.h
|
||||
rts/seL4/CMakeLists.txt
|
||||
rts/seL4/README.md
|
||||
|
||||
Extra-doc-files:
|
||||
CHANGELOG.md
|
||||
@ -86,13 +63,65 @@ Extra-doc-files:
|
||||
README.md
|
||||
RELEASE-CHECKS.md
|
||||
idris-tutorial.pdf
|
||||
samples/effects/*.idr
|
||||
samples/misc/*.idr
|
||||
samples/misc/*.lidr
|
||||
samples/tutorial/*.idr
|
||||
man/idris.1
|
||||
samples/**/*.idr
|
||||
samples/**/*.lidr
|
||||
|
||||
-- extra-source-files is generated by Setup.hs using `git --ls-files`.
|
||||
Extra-source-files:
|
||||
Makefile
|
||||
config.mk
|
||||
custom.mk-alldeps
|
||||
mkpkg.sh
|
||||
stack-alt.yaml
|
||||
stack-shell.nix
|
||||
stack.yaml
|
||||
stylize.sh
|
||||
win-release.sh
|
||||
|
||||
benchmarks/*.pl
|
||||
benchmarks/**/*.idr
|
||||
benchmarks/**/*.ipkg
|
||||
benchmarks/quasigroups/board
|
||||
|
||||
icons/*.png
|
||||
icons/*.ico
|
||||
icons/*.rc
|
||||
icons/*.svg
|
||||
icons/*.xml
|
||||
|
||||
libs/**/*.idr
|
||||
libs/**/*.ipkg
|
||||
libs/**/*.txt
|
||||
libs/Makefile
|
||||
libs/base/Makefile
|
||||
libs/contrib/Makefile
|
||||
libs/effects/Makefile
|
||||
libs/prelude/Makefile
|
||||
libs/pruviloj/Makefile
|
||||
|
||||
scripts/generate-multi-ghc-travis-template
|
||||
scripts/runidris
|
||||
scripts/runidris-node
|
||||
|
||||
src/.ghci
|
||||
|
||||
test/*.md
|
||||
test/*.hs
|
||||
test/**/*.idr
|
||||
test/**/*.lidr
|
||||
test/**/*.ipkg
|
||||
test/**/*.out
|
||||
test/**/*.sh
|
||||
test/**/*.c
|
||||
test/**/*.h
|
||||
test/**/*.in
|
||||
test/**/*.txt
|
||||
test/**/*.js
|
||||
test/base001/Makefile
|
||||
test/ffi004/theOtherType
|
||||
test/ffi004/theType
|
||||
test/scripts/timeout
|
||||
|
||||
source-repository head
|
||||
type: git
|
||||
@ -100,7 +129,7 @@ source-repository head
|
||||
|
||||
custom-setup
|
||||
setup-depends:
|
||||
Cabal >= 1.10 && <2.5,
|
||||
Cabal >= 2.4 && < 3.1,
|
||||
base >= 4 && <5,
|
||||
directory,
|
||||
filepath,
|
||||
@ -261,14 +290,17 @@ Library
|
||||
Util.Pretty
|
||||
, Util.Net
|
||||
|
||||
|
||||
|
||||
-- Auto Generated
|
||||
, Paths_idris
|
||||
, Version_idris
|
||||
, Tools_idris
|
||||
, BuildFlags_idris
|
||||
|
||||
-- Auto Generated
|
||||
Autogen-modules: Paths_idris
|
||||
, Version_idris
|
||||
, Tools_idris
|
||||
, BuildFlags_idris
|
||||
|
||||
Build-depends: base >=4 && <5
|
||||
, aeson >= 0.6 && < 1.5
|
||||
, annotated-wl-pprint >= 0.7 && < 0.8
|
||||
@ -280,7 +312,7 @@ Library
|
||||
, blaze-html >= 0.6.1.3 && < 0.10
|
||||
, blaze-markup >= 0.5.2.1 && < 0.9
|
||||
, bytestring < 0.11
|
||||
, cheapskate >= 0.1.1 && < 0.2
|
||||
, cheapskate >= 0.1.1.2 && < 0.2
|
||||
, code-page >= 0.1 && < 0.3
|
||||
, containers >= 0.5 && < 0.7
|
||||
, deepseq < 1.5
|
||||
@ -292,7 +324,7 @@ Library
|
||||
, megaparsec >= 7.0.4 && < 8
|
||||
, mtl >= 2.1 && < 2.3
|
||||
, network >= 2.7 && < 2.9
|
||||
, optparse-applicative >= 0.13 && < 0.15
|
||||
, optparse-applicative >= 0.13 && < 0.16
|
||||
, parser-combinators >= 1.0.0
|
||||
, pretty < 1.2
|
||||
, process < 1.7
|
||||
@ -300,8 +332,8 @@ Library
|
||||
, safe >= 0.3.9
|
||||
, split < 0.3
|
||||
, terminal-size < 0.4
|
||||
, text >=1.2.1.0 && < 1.3
|
||||
, time >= 1.4 && < 1.9
|
||||
, text >=1.2.1.0 && < 1.4
|
||||
, time >= 1.4 && < 2.0
|
||||
, transformers >= 0.5 && < 0.6
|
||||
, uniplate >=1.6 && < 1.7
|
||||
, unordered-containers < 0.3
|
||||
@ -313,7 +345,8 @@ Library
|
||||
, async < 2.3
|
||||
|
||||
if !impl(ghc >= 8.0)
|
||||
Build-Depends: semigroups == 0.18.*
|
||||
Build-Depends: semigroups == 0.18.*
|
||||
, fail == 4.9.0.*
|
||||
|
||||
Default-Language: Haskell2010
|
||||
ghc-prof-options: -auto-all -caf-all
|
||||
@ -332,6 +365,7 @@ Library
|
||||
cpp-options: -DIDRIS_GMP
|
||||
if flag(freestanding)
|
||||
other-modules: Target_idris
|
||||
autogen-modules: Target_idris
|
||||
cpp-options: -DFREESTANDING
|
||||
if flag(CI)
|
||||
ghc-options: -Werror
|
||||
@ -365,7 +399,7 @@ Test-suite regression-and-feature-tests
|
||||
, filepath
|
||||
, directory
|
||||
, haskeline >= 0.7
|
||||
, optparse-applicative >= 0.13 && < 0.15
|
||||
, optparse-applicative >= 0.13 && < 0.16
|
||||
, tagged
|
||||
, tasty >= 0.8
|
||||
, tasty-golden >= 2.0
|
||||
@ -380,6 +414,7 @@ Test-suite regression-and-feature-tests
|
||||
|
||||
Executable idris-codegen-c
|
||||
Main-is: Main.hs
|
||||
autogen-modules: Paths_idris
|
||||
other-modules: Paths_idris
|
||||
hs-source-dirs: codegen/idris-codegen-c
|
||||
|
||||
@ -395,6 +430,7 @@ Executable idris-codegen-c
|
||||
|
||||
Executable idris-codegen-javascript
|
||||
Main-is: Main.hs
|
||||
autogen-modules: Paths_idris
|
||||
other-modules: Paths_idris
|
||||
hs-source-dirs: codegen/idris-codegen-javascript
|
||||
|
||||
@ -410,6 +446,7 @@ Executable idris-codegen-javascript
|
||||
|
||||
Executable idris-codegen-node
|
||||
Main-is: Main.hs
|
||||
autogen-modules: Paths_idris
|
||||
other-modules: Paths_idris
|
||||
hs-source-dirs: codegen/idris-codegen-node
|
||||
|
||||
@ -422,3 +459,4 @@ Executable idris-codegen-node
|
||||
Default-Language: Haskell2010
|
||||
ghc-prof-options: -auto-all -caf-all
|
||||
ghc-options: -threaded -rtsopts -funbox-strict-fields
|
||||
|
||||
|
@ -18,6 +18,7 @@ import Idris.Info (getIdrisVersion)
|
||||
import Idris.Options
|
||||
import IRTS.CodegenCommon
|
||||
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
import Control.Monad.Trans (lift)
|
||||
import Control.Monad.Trans.Except (throwE)
|
||||
import Control.Monad.Trans.Reader (ask)
|
||||
@ -264,7 +265,7 @@ parseCodegen :: String -> Codegen
|
||||
parseCodegen "bytecode" = Bytecode
|
||||
parseCodegen cg = Via IBCFormat (map toLower cg)
|
||||
|
||||
parseLogCats :: Monad m => String -> m [LogCat]
|
||||
parseLogCats :: Fail.MonadFail m => String -> m [LogCat]
|
||||
parseLogCats s =
|
||||
case lastMay (readP_to_S doParse s) of
|
||||
Just (xs, _) -> return xs
|
||||
@ -290,7 +291,7 @@ parseLogCats s =
|
||||
s <- look
|
||||
fail $ "Category: " ++ s ++ " is not recognised."
|
||||
|
||||
parseConsoleWidth :: Monad m => String -> m ConsoleWidth
|
||||
parseConsoleWidth :: Fail.MonadFail m => String -> m ConsoleWidth
|
||||
parseConsoleWidth "auto" = return AutomaticWidth
|
||||
parseConsoleWidth "infinite" = return InfinitelyWide
|
||||
parseConsoleWidth s =
|
||||
|
@ -627,7 +627,7 @@ groupCons cs = gc [] cs
|
||||
PConst cval -> return $ addConG cval (ps, res) acc
|
||||
PSuc n -> return $ addg False CSuc [n] (ps, res) acc
|
||||
PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc
|
||||
pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
|
||||
pat -> error $ show pat ++ " is not a constructor or constant (can't happen)"
|
||||
|
||||
addg uniq c conargs res []
|
||||
= [ConGroup uniq c [(conargs, res)]]
|
||||
|
@ -70,6 +70,7 @@ import qualified Prelude as S (Semigroup(..))
|
||||
import Control.Applicative (Alternative, Applicative(..))
|
||||
import qualified Control.Applicative as A (Alternative(..))
|
||||
import Control.DeepSeq (($!!))
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Binary hiding (get, put)
|
||||
import Data.Char
|
||||
@ -324,6 +325,11 @@ bindTC x k = case x of
|
||||
instance Monad TC where
|
||||
return x = OK x
|
||||
x >>= k = bindTC x k
|
||||
#if !(MIN_VERSION_base(4,12,0))
|
||||
fail = Fail.fail
|
||||
#endif
|
||||
|
||||
instance Fail.MonadFail TC where
|
||||
fail e = Error (InternalMsg e)
|
||||
|
||||
instance MonadPlus TC where
|
||||
|
@ -36,6 +36,7 @@ import Idris.Core.TT (FC(..))
|
||||
import Idris.Output (Message(..))
|
||||
|
||||
import Control.Arrow (app)
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
import Control.Monad.State.Strict (StateT(..), evalStateT)
|
||||
import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..), listen,
|
||||
runWriterT, tell)
|
||||
@ -51,7 +52,7 @@ import qualified Util.Pretty as PP
|
||||
type Parser s = StateT s (WriterT FC (P.Parsec Void String))
|
||||
|
||||
-- | A constraint for parsing without state
|
||||
type Parsing m = (P.MonadParsec Void String m, MonadWriter FC m)
|
||||
type Parsing m = (Fail.MonadFail m, P.MonadParsec Void String m, MonadWriter FC m)
|
||||
|
||||
-- | Run the Idris parser stack
|
||||
runparser :: Parser st res -> st -> String -> String -> Either ParseError res
|
||||
|
@ -113,18 +113,18 @@ and somewhat self-explanatory.
|
||||
|
||||
1. Choose the family your test shall belong to and remember its identifier.
|
||||
2. Pick the next available integer in the test family. It will be the index.
|
||||
3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run` script.
|
||||
3. Say the family's identifier is `foo` and the index is `42`. You should call `./mktest.pl foo042` ; this will create the directory and a simple `run.sh` script.
|
||||
4. Modify the `run` script to your liking. If you want to call the idris executable, write `${IDRIS:-idris} $@`.
|
||||
5. Add any file you may need in the directory. If they don't end in `.idr`, you should remember them for the next step.
|
||||
6. Add your test in `TestData.hs`. Each family has a list of `(Index, CompatCodegen)`. See the next section for the available values in `CompatCodegen`. In most cases, you should write `( 42, ANY)`.
|
||||
7. Generate the `expected` file by doing:
|
||||
7. Generate the `expected.out` file by doing:
|
||||
```
|
||||
# Using cabal
|
||||
cabal test --test-options="--pattern foo042 --accept"
|
||||
# Using stack
|
||||
stack test --test-arguments="--pattern foo042 --accept"
|
||||
```
|
||||
8. Check the content of `expected`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.
|
||||
8. Check the content of `expected.out`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.
|
||||
|
||||
### Specifying compatible backends
|
||||
|
||||
@ -146,7 +146,7 @@ Currently, `NONE` has the same effect as `ANY`, but this will change.
|
||||
|
||||
### Updating golden files
|
||||
|
||||
To update the `expected` file for every test, do one of the following:
|
||||
To update the `expected.out` file for every test, do one of the following:
|
||||
|
||||
```
|
||||
# Using make
|
||||
@ -157,4 +157,4 @@ cabal test --test-options="--accept"
|
||||
stack test --test-arguments="--accept"
|
||||
```
|
||||
|
||||
"Accepted" tests are the ones that update the golden file. A test can still fail if the `run` script itself crashes.
|
||||
"Accepted" tests are the ones that update the golden file. A test can still fail if the `run.sh` script itself crashes.
|
||||
|
@ -62,7 +62,7 @@ ingredients = defaultIngredients ++
|
||||
test :: String -> String -> IO () -> TestTree
|
||||
test testName path = goldenVsFileDiff testName diff ref output
|
||||
where
|
||||
ref = path </> "expected"
|
||||
ref = path </> "expected.out"
|
||||
output = path </> "output"
|
||||
diff ref new | os == "openbsd" = ["diff", "-u", new, ref]
|
||||
| otherwise = ["diff", "--strip-trailing-cr", "-u", new, ref]
|
||||
@ -92,7 +92,7 @@ mkGoldenTests testFamilies flags =
|
||||
-- this thing.
|
||||
runTest :: String -> Flags -> IO ()
|
||||
runTest path flags = do
|
||||
let run = (proc "bash" ("run" : flags)) {cwd = Just path}
|
||||
let run = (proc "bash" ("run.sh" : flags)) {cwd = Just path}
|
||||
(_, output, error_out) <- readCreateProcessWithExitCode run ""
|
||||
writeFile (path </> "output") (normalise output)
|
||||
when (error_out /= "") $ hPutStrLn stderr ("\nError: " ++ path ++ "\n" ++ error_out)
|
||||
|
2
test/base001/run → test/base001/run.sh
Executable file → Normal file
2
test/base001/run → test/base001/run.sh
Executable file → Normal file
@ -3,7 +3,7 @@
|
||||
set -u
|
||||
|
||||
if [[ ${OSTYPE} = 'msys' ]]; then
|
||||
cat expected # skip this test on Windows
|
||||
cat expected.out # skip this test on Windows
|
||||
else
|
||||
${IDRIS:-idris} "$@" --build base001.ipkg | grep -v 'make.*:'
|
||||
./base001 2>&1 | grep -v '^sh:.*\./does-not-exist:'
|
0
test/basic001/run → test/basic001/run.sh
Executable file → Normal file
0
test/basic001/run → test/basic001/run.sh
Executable file → Normal file
0
test/basic002/run → test/basic002/run.sh
Executable file → Normal file
0
test/basic002/run → test/basic002/run.sh
Executable file → Normal file
0
test/basic003/run → test/basic003/run.sh
Executable file → Normal file
0
test/basic003/run → test/basic003/run.sh
Executable file → Normal file
0
test/basic004/run → test/basic004/run.sh
Executable file → Normal file
0
test/basic004/run → test/basic004/run.sh
Executable file → Normal file
0
test/basic005/run → test/basic005/run.sh
Executable file → Normal file
0
test/basic005/run → test/basic005/run.sh
Executable file → Normal file
0
test/basic006/run → test/basic006/run.sh
Executable file → Normal file
0
test/basic006/run → test/basic006/run.sh
Executable file → Normal file
0
test/basic007/run → test/basic007/run.sh
Executable file → Normal file
0
test/basic007/run → test/basic007/run.sh
Executable file → Normal file
0
test/basic008/run → test/basic008/run.sh
Executable file → Normal file
0
test/basic008/run → test/basic008/run.sh
Executable file → Normal file
0
test/basic009/run → test/basic009/run.sh
Executable file → Normal file
0
test/basic009/run → test/basic009/run.sh
Executable file → Normal file
0
test/basic010/run → test/basic010/run.sh
Executable file → Normal file
0
test/basic010/run → test/basic010/run.sh
Executable file → Normal file
0
test/basic011/run → test/basic011/run.sh
Executable file → Normal file
0
test/basic011/run → test/basic011/run.sh
Executable file → Normal file
0
test/basic012/run → test/basic012/run.sh
Executable file → Normal file
0
test/basic012/run → test/basic012/run.sh
Executable file → Normal file
0
test/basic013/run → test/basic013/run.sh
Executable file → Normal file
0
test/basic013/run → test/basic013/run.sh
Executable file → Normal file
0
test/basic014/run → test/basic014/run.sh
Executable file → Normal file
0
test/basic014/run → test/basic014/run.sh
Executable file → Normal file
0
test/basic015/run → test/basic015/run.sh
Executable file → Normal file
0
test/basic015/run → test/basic015/run.sh
Executable file → Normal file
0
test/basic016/run → test/basic016/run.sh
Executable file → Normal file
0
test/basic016/run → test/basic016/run.sh
Executable file → Normal file
0
test/basic017/run → test/basic017/run.sh
Executable file → Normal file
0
test/basic017/run → test/basic017/run.sh
Executable file → Normal file
0
test/basic018/run → test/basic018/run.sh
Executable file → Normal file
0
test/basic018/run → test/basic018/run.sh
Executable file → Normal file
0
test/basic019/run → test/basic019/run.sh
Executable file → Normal file
0
test/basic019/run → test/basic019/run.sh
Executable file → Normal file
0
test/basic020/run → test/basic020/run.sh
Executable file → Normal file
0
test/basic020/run → test/basic020/run.sh
Executable file → Normal file
0
test/basic021/run → test/basic021/run.sh
Executable file → Normal file
0
test/basic021/run → test/basic021/run.sh
Executable file → Normal file
0
test/basic022/run → test/basic022/run.sh
Executable file → Normal file
0
test/basic022/run → test/basic022/run.sh
Executable file → Normal file
0
test/basic023/run → test/basic023/run.sh
Executable file → Normal file
0
test/basic023/run → test/basic023/run.sh
Executable file → Normal file
@ -1,6 +1,6 @@
|
||||
#!/usr/bin/env bash
|
||||
|
||||
${IDRIS:-idris} $@ --quiet --port none < input
|
||||
${IDRIS:-idris} $@ --quiet --port none < input.in
|
||||
${IDRIS:-idris} $@ basic024.idr -o basic024
|
||||
|
||||
./basic024
|
4
test/basic025/run → test/basic025/run.sh
Executable file → Normal file
4
test/basic025/run → test/basic025/run.sh
Executable file → Normal file
@ -1,7 +1,7 @@
|
||||
#!/usr/bin/env bash
|
||||
${IDRIS:-idris} $@ --quiet --port none < input
|
||||
${IDRIS:-idris} $@ --quiet --port none < input.in
|
||||
${IDRIS:-idris} $@ -o basic025 basic025.idr
|
||||
|
||||
./basic025 input
|
||||
./basic025 input.in
|
||||
|
||||
rm -f basic025 *.ibc
|
0
test/bignum001/run → test/bignum001/run.sh
Executable file → Normal file
0
test/bignum001/run → test/bignum001/run.sh
Executable file → Normal file
0
test/bignum002/run → test/bignum002/run.sh
Executable file → Normal file
0
test/bignum002/run → test/bignum002/run.sh
Executable file → Normal file
0
test/bignum003/run → test/bignum003/run.sh
Executable file → Normal file
0
test/bignum003/run → test/bignum003/run.sh
Executable file → Normal file
0
test/bounded001/run → test/bounded001/run.sh
Executable file → Normal file
0
test/bounded001/run → test/bounded001/run.sh
Executable file → Normal file
0
test/buffer001/run → test/buffer001/run.sh
Executable file → Normal file
0
test/buffer001/run → test/buffer001/run.sh
Executable file → Normal file
0
test/buffer002/run → test/buffer002/run.sh
Executable file → Normal file
0
test/buffer002/run → test/buffer002/run.sh
Executable file → Normal file
0
test/contrib001/run → test/contrib001/run.sh
Executable file → Normal file
0
test/contrib001/run → test/contrib001/run.sh
Executable file → Normal file
0
test/corecords001/run → test/corecords001/run.sh
Executable file → Normal file
0
test/corecords001/run → test/corecords001/run.sh
Executable file → Normal file
0
test/corecords002/run → test/corecords002/run.sh
Executable file → Normal file
0
test/corecords002/run → test/corecords002/run.sh
Executable file → Normal file
2
test/delab001/run → test/delab001/run.sh
Executable file → Normal file
2
test/delab001/run → test/delab001/run.sh
Executable file → Normal file
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input
|
||||
${IDRIS:-idris} $@ --quiet --port none --nocolor delab001.idr < input.in
|
||||
rm -f *.ibc
|
0
test/directives001/run → test/directives001/run.sh
Executable file → Normal file
0
test/directives001/run → test/directives001/run.sh
Executable file → Normal file
0
test/directives003/run → test/directives003/run.sh
Executable file → Normal file
0
test/directives003/run → test/directives003/run.sh
Executable file → Normal file
0
test/disambig002/run → test/disambig002/run.sh
Executable file → Normal file
0
test/disambig002/run → test/disambig002/run.sh
Executable file → Normal file
2
test/docs001/run → test/docs001/run.sh
Executable file → Normal file
2
test/docs001/run → test/docs001/run.sh
Executable file → Normal file
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input
|
||||
${IDRIS:-idris} $@ --quiet --port none --nocolor docs001.idr < input.in
|
||||
rm *.ibc
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user