search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.51k stars 374 forks source link

Step 2 of the build process fails with reordering issues in the testing stages. #871

Closed nothingnesses closed 3 years ago

nothingnesses commented 3 years ago

Please check INSTALL.md and README.md to ensure you have all the required dependencies. In particular, you need a version of Chez Scheme compiled with threading support (this is the default in most distributions) in order to run the tests successfully.

Some common possible solutions:

Otherwise, please describe the problem, including any relevant parts of build logs, and describing as much about your environment as possible.

System

(Click to expand) ``` $ uname -a Linux a 5.9.14_1 #1 SMP 1607917304 x86_64 GNU/Linux $ lsb_release -a LSB Version: 1.0 Distributor ID: VoidLinux Description: Void Linux Release: rolling Codename: void $ make --version GNU Make 4.3 Built for x86_64-unknown-linux-musl Copyright (C) 1988-2020 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. $ realpath --version realpath (GNU coreutils) 8.32 Copyright (C) 2020 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later . This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. Written by Padraig Brady. $ bash --version GNU bash, version 5.0.18(1)-release (x86_64-unknown-linux-musl) Copyright (C) 2019 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later This is free software; you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. $ cc --version cc (GCC) 9.3.0 Copyright (C) 2019 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. $ scheme --version 9.5.4 $ node --version v14.13.1 ```

System is musl Void. scheme is pkgsCross.musl64.chez from nix.

Reproduction

(Click to expand) ```Shell sudo xbps-install -S nix sudo ln -s /etc/sv/nix-daemon /var/service/ sudo sv start nix-daemon nix-channel --add https://nixos.org/channels/nixpkgs-unstable nix-channel --update # Install the `chez` package with `musl` compatibility. nix-env -f channel:nixos-unstable -iA pkgsCross.musl64.chez # Confirm that `scheme` is the one supplied by `nix`. which scheme # /home/a/.nix-profile/bin/scheme # Confirm that `idris2` isn't in PATH. which idris2 # which: no idris2 in (/home/a/.cargo/bin:/home/a/.npm-global/bin:/home/a/.idris2/bin:/home/a/.local/bin:/bedrock/cross/pin/bin:/bedrock/bin:/usr/local/bin:/usr/local/sbin:/usr/bin:/usr/sbin:/bin:/sbin:/usr/local/games:/usr/games:/home/a/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/home/a/.cargo/bin:/home/a/.npm-global/bin:/home/a/.idris2/bin:/home/a/.local/bin:/bedrock/cross/bin) # Confirm `~/.idris2` doesn't exist. ls ~/.idris2 # "/home/a/.idris2": No such file or directory (os error 2) curl -O https://www.idris-lang.org/idris2-src/idris2-latest.tgz tar xf idris2-latest.tgz cd Idris2-0.2.1 # Step 1 of the `idris2` build steps. export PATH="$HOME/.idris2/bin:$PATH" export LD_LIBRARY_PATH="$HOME/.idris2/lib:$LD_LIBRARY_PATH" # Step 2 of the `idris2` build steps with additional logging. make bootstrap SCHEME=scheme 2>&1 | tee ~/"make bootstrap SCHEME=scheme" ```

Expected behaviour

Step 2 of INSTALL.md is successful.

Actual behaviour

Step 2 fails with reordering issues in the testing stages. The contents of ~/"make bootstrap SCHEME=scheme" is:

(Click to expand) ``` make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' cc -Wall -fPIC -O2 -c -o getline.o getline.c cc -Wall -fPIC -O2 -c -o idris_buffer.o idris_buffer.c cc -Wall -fPIC -O2 -c -o idris_directory.o idris_directory.c cc -Wall -fPIC -O2 -c -o idris_file.o idris_file.c cc -Wall -fPIC -O2 -c -o idris_net.o idris_net.c cc -Wall -fPIC -O2 -c -o idris_support.o idris_support.c ar rc libidris2_support.a getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o ranlib libidris2_support.a cc -shared -o libidris2_support.so getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' cp support/c/libidris2_support.so bootstrap/idris2_app sed s/libidris2_support.so/libidris2_support.so/g bootstrap/idris2_app/idris2.ss > bootstrap/idris2_app/idris2-boot.ss sed -i 's|__PREFIX__|/home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss sh ./bootstrap.sh bootstrapping SCHEME=scheme IDRIS2_VERSION=0.2.1 Building idris2-boot from idris2-boot.ss compiling idris2_app/idris2-boot.ss with output to idris2_app/idris2-boot.so /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make -C libs/prelude IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' ../../build/exec/idris2 --build prelude.ipkg 1/12: Building Builtin (Builtin.idr) 2/12: Building PrimIO (PrimIO.idr) 3/12: Building Prelude.Basics (Prelude/Basics.idr) 4/12: Building Prelude.Ops (Prelude/Ops.idr) 5/12: Building Prelude.EqOrd (Prelude/EqOrd.idr) 6/12: Building Prelude.Num (Prelude/Num.idr) 7/12: Building Prelude.Interfaces (Prelude/Interfaces.idr) 8/12: Building Prelude.Uninhabited (Prelude/Uninhabited.idr) 9/12: Building Prelude.Types (Prelude/Types.idr) 10/12: Building Prelude.Show (Prelude/Show.idr) 11/12: Building Prelude.IO (Prelude/IO.idr) 12/12: Building Prelude (Prelude.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' make -C libs/base IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' ../../build/exec/idris2 --build base.ipkg 1/47: Building Data.Nat (Data/Nat.idr) 2/47: Building Data.List1 (Data/List1.idr) 3/47: Building Data.List (Data/List.idr) 4/47: Building Data.Strings (Data/Strings.idr) 5/47: Building System.Info (System/Info.idr) 6/47: Building System.File (System/File.idr) 7/47: Building System.REPL (System/REPL.idr) 8/47: Building System.FFI (System/FFI.idr) 9/47: Building System.Clock (System/Clock.idr) 10/47: Building System.Concurrency.Raw (System/Concurrency/Raw.idr) 11/47: Building Data.Bool (Data/Bool.idr) 12/47: Building Data.So (Data/So.idr) 13/47: Building System (System.idr) 14/47: Building Language.Reflection.TT (Language/Reflection/TT.idr) 15/47: Building Language.Reflection.TTImp (Language/Reflection/TTImp.idr) 16/47: Building Language.Reflection (Language/Reflection.idr) 17/47: Building Debug.Trace (Debug/Trace.idr) 18/47: Building Data.Maybe (Data/Maybe.idr) 19/47: Building Data.Either (Data/Either.idr) 20/47: Building Decidable.Equality (Decidable/Equality.idr) 21/47: Building Data.Fin (Data/Fin.idr) 22/47: Building Data.Vect (Data/Vect.idr) 23/47: Building Data.Vect.Elem (Data/Vect/Elem.idr) 24/47: Building Data.Stream (Data/Stream.idr) 25/47: Building Data.IORef (Data/IORef.idr) 26/47: Building Control.Monad.ST (Control/Monad/ST.idr) 27/47: Building Data.Ref (Data/Ref.idr) 28/47: Building Data.Primitives.Views (Data/Primitives/Views.idr) 29/47: Building Data.Morphisms (Data/Morphisms.idr) 30/47: Building Data.List.Elem (Data/List/Elem.idr) 31/47: Building Data.List.Quantifiers (Data/List/Quantifiers.idr) 32/47: Building Control.WellFounded (Control/WellFounded.idr) 33/47: Building Data.Nat.Views (Data/Nat/Views.idr) 34/47: Building Data.List.Views (Data/List/Views.idr) 35/47: Building Data.IOArray.Prims (Data/IOArray/Prims.idr) 36/47: Building Data.IOArray (Data/IOArray.idr) 37/47: Building Data.Fuel (Data/Fuel.idr) 38/47: Building Data.DPair (Data/DPair.idr) 39/47: Building System.Directory (System/Directory.idr) 40/47: Building Data.Buffer (Data/Buffer.idr) 41/47: Building Data.Bool.Xor (Data/Bool/Xor.idr) 42/47: Building Control.Monad.Identity (Control/Monad/Identity.idr) 43/47: Building Control.Monad.Trans (Control/Monad/Trans.idr) 44/47: Building Control.Monad.State (Control/Monad/State.idr) 45/47: Building Control.App (Control/App.idr) 46/47: Building Control.App.FileIO (Control/App/FileIO.idr) 47/47: Building Control.App.Console (Control/App/Console.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' make -C libs/contrib IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' ../../build/exec/idris2 --build contrib.ipkg 1/60: Building Data.String.Extra (Data/String/Extra.idr) 2/60: Building Text.Token (Text/Token.idr) 3/60: Building Control.Delayed (Control/Delayed.idr) 4/60: Building Text.Lexer.Core (Text/Lexer/Core.idr) 5/60: Building Text.Quantity (Text/Quantity.idr) 6/60: Building Text.Lexer (Text/Lexer.idr) 7/60: Building Text.Parser.Core (Text/Parser/Core.idr) 8/60: Building Text.Parser (Text/Parser.idr) 9/60: Building System.Path (System/Path.idr) 10/60: Building System.Random (System/Random.idr) 11/60: Building Control.ANSI.CSI (Control/ANSI/CSI.idr) 12/60: Building Control.ANSI.SGR (Control/ANSI/SGR.idr) 13/60: Building Control.ANSI (Control/ANSI.idr) 14/60: Building Text.PrettyPrint.Prettyprinter.Doc (Text/PrettyPrint/Prettyprinter/Doc.idr) 15/60: Building Text.PrettyPrint.Prettyprinter.Render.Terminal (Text/PrettyPrint/Prettyprinter/Render/Terminal.idr) 16/60: Building Text.PrettyPrint.Prettyprinter.SimpleDocTree (Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr) 17/60: Building Text.PrettyPrint.Prettyprinter.Render.String (Text/PrettyPrint/Prettyprinter/Render/String.idr) 18/60: Building Text.PrettyPrint.Prettyprinter.Util (Text/PrettyPrint/Prettyprinter/Util.idr) 19/60: Building Text.PrettyPrint.Prettyprinter.Symbols (Text/PrettyPrint/Prettyprinter/Symbols.idr) 20/60: Building Text.PrettyPrint.Prettyprinter (Text/PrettyPrint/Prettyprinter.idr) 21/60: Building Language.JSON.String.Tokens (Language/JSON/String/Tokens.idr) 22/60: Building Language.JSON.String.Lexer (Language/JSON/String/Lexer.idr) 23/60: Building Language.JSON.String.Parser (Language/JSON/String/Parser.idr) 24/60: Building Language.JSON.String (Language/JSON/String.idr) 25/60: Building Language.JSON.Tokens (Language/JSON/Tokens.idr) 26/60: Building Language.JSON.Lexer (Language/JSON/Lexer.idr) 27/60: Building Language.JSON.Data (Language/JSON/Data.idr) 28/60: Building Language.JSON.Parser (Language/JSON/Parser.idr) 29/60: Building Language.JSON (Language/JSON.idr) 30/60: Building Debug.Buffer (Debug/Buffer.idr) 31/60: Building Data.Vect.Sort (Data/Vect/Sort.idr) 32/60: Building Data.String.Parser (Data/String/Parser.idr) 33/60: Building Data.String.Interpolation (Data/String/Interpolation.idr) 34/60: Building Data.SortedMap (Data/SortedMap.idr) 35/60: Building Data.SortedSet (Data/SortedSet.idr) 36/60: Building Data.Nat.Fib (Data/Nat/Fib.idr) 37/60: Building Data.Fin.Extra (Data/Fin/Extra.idr) 38/60: Building Data.Nat.Equational (Data/Nat/Equational.idr) 39/60: Building Syntax.PreorderReasoning (Syntax/PreorderReasoning.idr) 40/60: Building Data.Nat.Factor (Data/Nat/Factor.idr) 41/60: Building Data.Nat.Fact (Data/Nat/Fact.idr) 42/60: Building Data.Nat.Ack (Data/Nat/Ack.idr) 43/60: Building Control.Algebra (Control/Algebra.idr) 44/60: Building Data.Nat.Algebra (Data/Nat/Algebra.idr) 45/60: Building Data.Morphisms.Algebra (Data/Morphisms/Algebra.idr) 46/60: Building Data.Logic.Propositional (Data/Logic/Propositional.idr) 47/60: Building Data.List.Equalities (Data/List/Equalities.idr) 48/60: Building Data.List.Reverse (Data/List/Reverse.idr) 49/60: Building Data.List.Views.Extra (Data/List/Views/Extra.idr) 50/60: Building Data.List.Palindrome (Data/List/Palindrome.idr) 51/60: Building Syntax.WithProof (Syntax/WithProof.idr) 52/60: Building Data.List.TailRec (Data/List/TailRec.idr) 53/60: Building Data.List.Algebra (Data/List/Algebra.idr) 54/60: Building Data.Linear.Array (Data/Linear/Array.idr) 55/60: Building Data.Bool.Algebra (Data/Bool/Algebra.idr) 56/60: Building Control.Algebra.Implementations (Control/Algebra/Implementations.idr) 57/60: Building Control.Algebra.Laws (Control/Algebra/Laws.idr) 58/60: Building Control.Monad.Syntax (Control/Monad/Syntax.idr) 59/60: Building Control.Monad.Algebra (Control/Monad/Algebra.idr) 60/60: Building Control.Linear.LIO (Control/Linear/LIO.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' make -C libs/network IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' ../../build/exec/idris2 --build network.ipkg 1/5: Building Network.Socket.Data (Network/Socket/Data.idr) 2/5: Building Network.FFI (Network/FFI.idr) 3/5: Building Network.Socket.Raw (Network/Socket/Raw.idr) 4/5: Building Network.Socket (Network/Socket.idr) 5/5: Building Control.Linear.Network (Control/Linear/Network.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1' mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/bin/ install build/exec/idris2 /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/bin mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/lib/ install support/c/libidris2_support.so /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/lib mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/bin/idris2_app install build/exec/idris2_app/* /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/bin/idris2_app mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/chez mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/racket mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/gambit mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/js install support/chez/* /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/chez install support/racket/* /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/racket install support/gambit/* /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/gambit install support/js/* /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support/js make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' mkdir -p /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/lib install libidris2_support.a libidris2_support.so /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/lib make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' make -C libs/prelude install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' ../../build/exec/idris2 --install prelude.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Builtin.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/PrimIO.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/Basics.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/EqOrd.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/Interfaces.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/IO.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/Num.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/Ops.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/Show.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/Types.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc/Prelude/Uninhabited.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/prelude/Prelude make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' make -C libs/base install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' ../../build/exec/idris2 --install base.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/App.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/App/Console.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control/App Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/App/FileIO.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control/App Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/Monad/Identity.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/Monad/ST.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/Monad/State.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/Monad/Trans.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Control/WellFounded.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Control Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Bool.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Bool/Xor.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/Bool Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Buffer.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/DPair.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Either.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Fin.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Fuel.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/IOArray.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/IOArray/Prims.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/IOArray Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/IORef.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/List.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/List/Elem.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/List/Views.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/List/Quantifiers.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/List1.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Maybe.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Morphisms.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Nat.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Nat/Views.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Primitives/Views.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/Primitives Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Ref.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/So.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Stream.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Strings.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Vect.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Data/Vect/Elem.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Data/Vect Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Debug/Trace.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Debug Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Decidable/Equality.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Decidable Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Language/Reflection.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Language Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Language/Reflection/TT.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Language/Reflection Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/Language/Reflection/TTImp.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/Language/Reflection Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System/Concurrency/Raw.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/System/Concurrency Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System/Clock.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/System Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System/Directory.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/System Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System/File.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/System Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System/FFI.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/System Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System/Info.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/System Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc/System/REPL.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/base/System make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' make -C libs/contrib install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' ../../build/exec/idris2 --install contrib.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/ANSI.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/ANSI/SGR.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control/ANSI Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/ANSI/CSI.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control/ANSI Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/Delayed.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/Linear/LIO.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control/Linear Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/Monad/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/Monad/Syntax.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/Algebra/Laws.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control/Algebra Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Control/Algebra/Implementations.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Control/Algebra Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Bool/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Bool Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Linear/Array.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Linear Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/List/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/List/TailRec.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/List/Equalities.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/List/Reverse.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/List/Views/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/List/Views Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/List/Palindrome.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Fin/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Fin Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Logic/Propositional.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Logic Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Morphisms/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Morphisms Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Nat/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Nat/Ack.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Nat/Equational.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Nat/Fact.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Nat/Factor.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Nat/Fib.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/SortedMap.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/SortedSet.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/String/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/String Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/String/Interpolation.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/String Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/String/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/String Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Data/Vect/Sort.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Data/Vect Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Debug/Buffer.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Debug Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/Data.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/Lexer.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/String.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/String/Lexer.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON/String Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/String/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON/String Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/String/Tokens.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON/String Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Language/JSON/Tokens.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/Token.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/Quantity.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/Lexer.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/Parser/Core.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/Parser Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/Lexer/Core.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/Lexer Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/PrettyPrint Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Doc.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Symbols.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Util.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/SimpleDocTree.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Render/String.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/PrettyPrint/Prettyprinter/Render Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Render/Terminal.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Text/PrettyPrint/Prettyprinter/Render Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/System/Random.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/System Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/System/Path.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/System Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Syntax/WithProof.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Syntax Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc/Syntax/PreorderReasoning.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/contrib/Syntax make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' make -C libs/network install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' ../../build/exec/idris2 --install network.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc/Control/Linear/Network.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/network/Control/Linear Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc/Network/Socket.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/network/Network Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc/Network/Socket/Data.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/network/Network/Socket Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc/Network/Socket/Raw.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/network/Network/Socket Installing /home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc/Network/FFI.ttc to /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/network/Network make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make -C libs/prelude clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' make -C libs/base clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' make -C libs/contrib clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' make -C libs/network clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' rm -f getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o libidris2_support.so libidris2_support.a make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/bin/idris2 --clean idris2.ipkg Removed: /home/a/documents/projects/idris2/Idris2-0.2.1/build/exec/idris2 rm -f src/IdrisPaths.idr make -C tests clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/tests' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/tests' rm -f -r build make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' cc -Wall -fPIC -O2 -c -o getline.o getline.c cc -Wall -fPIC -O2 -c -o idris_buffer.o idris_buffer.c cc -Wall -fPIC -O2 -c -o idris_directory.o idris_directory.c cc -Wall -fPIC -O2 -c -o idris_file.o idris_file.c cc -Wall -fPIC -O2 -c -o idris_net.o idris_net.c cc -Wall -fPIC -O2 -c -o idris_support.o idris_support.c ar rc libidris2_support.a getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o ranlib libidris2_support.a cc -shared -o libidris2_support.so getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/support/c' echo 'module IdrisPaths' > src/IdrisPaths.idr echo 'export idrisVersion : ((Nat,Nat,Nat), String); idrisVersion = ((0,2,1), "")' >> src/IdrisPaths.idr echo 'export yprefix : String; yprefix="/home/a/.idris2"' >> src/IdrisPaths.idr /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/bin/idris2 --build idris2.ipkg 1/153: Building Core.FC (src/Core/FC.idr) 2/153: Building Core.Name (src/Core/Name.idr) 3/153: Building Data.Bool.Extra (src/Data/Bool/Extra.idr) 4/153: Building Data.NameMap (src/Data/NameMap.idr) 5/153: Building Algebra.Semiring (src/Algebra/Semiring.idr) 6/153: Building Algebra.Preorder (src/Algebra/Preorder.idr) 7/153: Building Algebra.ZeroOneOmega (src/Algebra/ZeroOneOmega.idr) 8/153: Building Algebra (src/Algebra.idr) 9/153: Building Core.TT (src/Core/TT.idr) 10/153: Building Core.CompileExpr (src/Core/CompileExpr.idr) 11/153: Building Core.CaseTree (src/Core/CaseTree.idr) 12/153: Building Core.Env (src/Core/Env.idr) 13/153: Building Text.Lexer.Core (src/Text/Lexer/Core.idr) 14/153: Building Text.Quantity (src/Text/Quantity.idr) 15/153: Building Text.Token (src/Text/Token.idr) 16/153: Building Text.Lexer (src/Text/Lexer.idr) 17/153: Building Parser.Lexer.Common (src/Parser/Lexer/Common.idr) 18/153: Building Utils.Hex (src/Utils/Hex.idr) 19/153: Building Utils.Octal (src/Utils/Octal.idr) 20/153: Building Utils.String (src/Utils/String.idr) 21/153: Building Parser.Lexer.Source (src/Parser/Lexer/Source.idr) 22/153: Building Text.Parser.Core (src/Text/Parser/Core.idr) 23/153: Building Text.Parser (src/Text/Parser.idr) 24/153: Building Parser.Rule.Common (src/Parser/Rule/Common.idr) 25/153: Building Text.Literate (src/Text/Literate.idr) 26/153: Building Parser.Unlit (src/Parser/Unlit.idr) 27/153: Building Parser.Support (src/Parser/Support.idr) 28/153: Building Parser.Rule.Source (src/Parser/Rule/Source.idr) 29/153: Building Utils.Either (src/Utils/Either.idr) 30/153: Building Parser.Source (src/Parser/Source.idr) 31/153: Building Core.Core (src/Core/Core.idr) 32/153: Building Core.Hash (src/Core/Hash.idr) 33/153: Building Utils.Binary (src/Utils/Binary.idr) 34/153: Building Utils.Path (src/Utils/Path.idr) 35/153: Building Core.Options (src/Core/Options.idr) 36/153: Building Data.IntMap (src/Data/IntMap.idr) 37/153: Building Data.StringMap (src/Data/StringMap.idr) 38/153: Building Core.Context (src/Core/Context.idr) 39/153: Building Compiler.LambdaLift (src/Compiler/LambdaLift.idr) 40/153: Building Compiler.ANF (src/Compiler/ANF.idr) 41/153: Building Core.Value (src/Core/Value.idr) 42/153: Building Core.Primitives (src/Core/Primitives.idr) 43/153: Building Core.Normalise (src/Core/Normalise.idr) 44/153: Building Compiler.CompileExpr (src/Compiler/CompileExpr.idr) 45/153: Building Data.LengthMatch (src/Data/LengthMatch.idr) 46/153: Building Compiler.Inline (src/Compiler/Inline.idr) 47/153: Building Compiler.VMCode (src/Compiler/VMCode.idr) 48/153: Building Core.Directory (src/Core/Directory.idr) 49/153: Building Core.TTC (src/Core/TTC.idr) 50/153: Building Compiler.Common (src/Compiler/Common.idr) 51/153: Building Core.InitPrimitives (src/Core/InitPrimitives.idr) 52/153: Building Core.UnifyState (src/Core/UnifyState.idr) 53/153: Building Core.Binary (src/Core/Binary.idr) 54/153: Building Core.Metadata (src/Core/Metadata.idr) 55/153: Building Core.GetType (src/Core/GetType.idr) 56/153: Building Core.Unify (src/Core/Unify.idr) 57/153: Building IdrisPaths (src/IdrisPaths.idr) 58/153: Building Idris.Version (src/Idris/Version.idr) 59/153: Building Idris.CommandLine (src/Idris/CommandLine.idr) 60/153: Building Compiler.Scheme.Common (src/Compiler/Scheme/Common.idr) 61/153: Building Compiler.Scheme.Chez (src/Compiler/Scheme/Chez.idr) 62/153: Building Compiler.Scheme.Racket (src/Compiler/Scheme/Racket.idr) 63/153: Building Compiler.Scheme.Gambit (src/Compiler/Scheme/Gambit.idr) 64/153: Building Core.AutoSearch (src/Core/AutoSearch.idr) 65/153: Building Data.ANameMap (src/Data/ANameMap.idr) 66/153: Building TTImp.TTImp (src/TTImp/TTImp.idr) 67/153: Building Idris.Syntax (src/Idris/Syntax.idr) 68/153: Building TTImp.Utils (src/TTImp/Utils.idr) 69/153: Building TTImp.Unelab (src/TTImp/Unelab.idr) 70/153: Building Idris.Resugar (src/Idris/Resugar.idr) 71/153: Building Idris.DocString (src/Idris/DocString.idr) 72/153: Building TTImp.BindImplicits (src/TTImp/BindImplicits.idr) 73/153: Building Core.LinearCheck (src/Core/LinearCheck.idr) 74/153: Building TTImp.Elab.Check (src/TTImp/Elab/Check.idr) 75/153: Building TTImp.Elab.Delayed (src/TTImp/Elab/Delayed.idr) 76/153: Building Core.Reflect (src/Core/Reflect.idr) 77/153: Building TTImp.Elab.Ambiguity (src/TTImp/Elab/Ambiguity.idr) 78/153: Building TTImp.Elab.App (src/TTImp/Elab/App.idr) 79/153: Building TTImp.Elab.ImplicitBind (src/TTImp/Elab/ImplicitBind.idr) 80/153: Building TTImp.Elab.As (src/TTImp/Elab/As.idr) 81/153: Building TTImp.Elab.Binders (src/TTImp/Elab/Binders.idr) 82/153: Building TTImp.Elab.Case (src/TTImp/Elab/Case.idr) 83/153: Building TTImp.Elab.Dot (src/TTImp/Elab/Dot.idr) 84/153: Building TTImp.Elab.Hole (src/TTImp/Elab/Hole.idr) 85/153: Building TTImp.Elab.Lazy (src/TTImp/Elab/Lazy.idr) 86/153: Building TTImp.Elab.Utils (src/TTImp/Elab/Utils.idr) 87/153: Building TTImp.Elab.Local (src/TTImp/Elab/Local.idr) 88/153: Building TTImp.Elab.Prim (src/TTImp/Elab/Prim.idr) 89/153: Building TTImp.Reflect (src/TTImp/Reflect.idr) 90/153: Building TTImp.Elab.Quote (src/TTImp/Elab/Quote.idr) 91/153: Building TTImp.Elab.Record (src/TTImp/Elab/Record.idr) 92/153: Building TTImp.Elab.Rewrite (src/TTImp/Elab/Rewrite.idr) 93/153: Building TTImp.Elab.RunElab (src/TTImp/Elab/RunElab.idr) 94/153: Building TTImp.Elab.Term (src/TTImp/Elab/Term.idr) 95/153: Building TTImp.Elab (src/TTImp/Elab.idr) 96/153: Building Core.Termination (src/Core/Termination.idr) 97/153: Building TTImp.Parser (src/TTImp/Parser.idr) 98/153: Building TTImp.ProcessData (src/TTImp/ProcessData.idr) 99/153: Building Core.CaseBuilder (src/Core/CaseBuilder.idr) 100/153: Building Core.Coverage (src/Core/Coverage.idr) 101/153: Building Core.Transform (src/Core/Transform.idr) 102/153: Building TTImp.Impossible (src/TTImp/Impossible.idr) 103/153: Building TTImp.PartialEval (src/TTImp/PartialEval.idr) 104/153: Building TTImp.WithClause (src/TTImp/WithClause.idr) 105/153: Building TTImp.ProcessDef (src/TTImp/ProcessDef.idr) 106/153: Building TTImp.ProcessParams (src/TTImp/ProcessParams.idr) 107/153: Building TTImp.ProcessRecord (src/TTImp/ProcessRecord.idr) 108/153: Building TTImp.ProcessRunElab (src/TTImp/ProcessRunElab.idr) 109/153: Building TTImp.ProcessTransform (src/TTImp/ProcessTransform.idr) 110/153: Building TTImp.ProcessType (src/TTImp/ProcessType.idr) 111/153: Building TTImp.ProcessDecls (src/TTImp/ProcessDecls.idr) 112/153: Building Idris.Elab.Implementation (src/Idris/Elab/Implementation.idr) 113/153: Building Idris.Elab.Interface (src/Idris/Elab/Interface.idr) 114/153: Building Utils.Shunting (src/Utils/Shunting.idr) 115/153: Building Idris.Desugar (src/Idris/Desugar.idr) 116/153: Building TTImp.Interactive.CaseSplit (src/TTImp/Interactive/CaseSplit.idr) 117/153: Building TTImp.Interactive.ExprSearch (src/TTImp/Interactive/ExprSearch.idr) 118/153: Building Idris.REPLOpts (src/Idris/REPLOpts.idr) 119/153: Building Data.List.Extra (src/Data/List/Extra.idr) 120/153: Building Idris.Error (src/Idris/Error.idr) 121/153: Building Idris.Parser (src/Idris/Parser.idr) 122/153: Building Idris.IDEMode.Commands (src/Idris/IDEMode/Commands.idr) 123/153: Building Idris.REPLCommon (src/Idris/REPLCommon.idr) 124/153: Building Idris.ProcessIdr (src/Idris/ProcessIdr.idr) 125/153: Building Idris.ModTree (src/Idris/ModTree.idr) 126/153: Building Data.These (src/Data/These.idr) 127/153: Building Data.StringTrie (src/Data/StringTrie.idr) 128/153: Building Parser.Lexer.Package (src/Parser/Lexer/Package.idr) 129/153: Building Parser.Rule.Package (src/Parser/Rule/Package.idr) 130/153: Building Parser.Package (src/Parser/Package.idr) 131/153: Building Compiler.ES.ImperativeAst (src/Compiler/ES/ImperativeAst.idr) 132/153: Building Compiler.ES.RemoveUnused (src/Compiler/ES/RemoveUnused.idr) 133/153: Building Compiler.ES.TailRec (src/Compiler/ES/TailRec.idr) 134/153: Building Compiler.ES.Imperative (src/Compiler/ES/Imperative.idr) 135/153: Building Compiler.ES.ES (src/Compiler/ES/ES.idr) 136/153: Building Compiler.ES.Node (src/Compiler/ES/Node.idr) 137/153: Building Compiler.ES.Javascript (src/Compiler/ES/Javascript.idr) 138/153: Building Idris.IDEMode.TokenLine (src/Idris/IDEMode/TokenLine.idr) 139/153: Building Idris.IDEMode.CaseSplit (src/Idris/IDEMode/CaseSplit.idr) 140/153: Building Idris.IDEMode.MakeClause (src/Idris/IDEMode/MakeClause.idr) 141/153: Building Idris.IDEMode.Holes (src/Idris/IDEMode/Holes.idr) 142/153: Building TTImp.Interactive.GenerateDef (src/TTImp/Interactive/GenerateDef.idr) 143/153: Building TTImp.Interactive.MakeLemma (src/TTImp/Interactive/MakeLemma.idr) 144/153: Building Idris.REPL (src/Idris/REPL.idr) 145/153: Building Idris.SetOptions (src/Idris/SetOptions.idr) 146/153: Building Idris.Package (src/Idris/Package.idr) 147/153: Building Idris.IDEMode.Parser (src/Idris/IDEMode/Parser.idr) 148/153: Building Idris.IDEMode.SyntaxHighlight (src/Idris/IDEMode/SyntaxHighlight.idr) 149/153: Building Idris.IDEMode.REPL (src/Idris/IDEMode/REPL.idr) 150/153: Building Yaffle.REPL (src/Yaffle/REPL.idr) 151/153: Building Yaffle.Main (src/Yaffle/Main.idr) 152/153: Building Idris.Driver (src/Idris/Driver.idr) 153/153: Building Idris.Main (src/Idris/Main.idr) make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/tests' /home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/bin/idris2 --build tests.ipkg 1/1: Building Main (Main.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/tests' make -C libs/prelude IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' ../../build/exec/idris2 --build prelude.ipkg 1/12: Building Builtin (Builtin.idr) 2/12: Building PrimIO (PrimIO.idr) 3/12: Building Prelude.Basics (Prelude/Basics.idr) 4/12: Building Prelude.Ops (Prelude/Ops.idr) 5/12: Building Prelude.EqOrd (Prelude/EqOrd.idr) 6/12: Building Prelude.Num (Prelude/Num.idr) 7/12: Building Prelude.Interfaces (Prelude/Interfaces.idr) 8/12: Building Prelude.Uninhabited (Prelude/Uninhabited.idr) 9/12: Building Prelude.Types (Prelude/Types.idr) 10/12: Building Prelude.Show (Prelude/Show.idr) 11/12: Building Prelude.IO (Prelude/IO.idr) 12/12: Building Prelude (Prelude.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude' make -C libs/base IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' ../../build/exec/idris2 --build base.ipkg 1/47: Building Data.Nat (Data/Nat.idr) 2/47: Building Data.List1 (Data/List1.idr) 3/47: Building Data.List (Data/List.idr) 4/47: Building Data.Strings (Data/Strings.idr) 5/47: Building System.Info (System/Info.idr) 6/47: Building System.File (System/File.idr) 7/47: Building System.REPL (System/REPL.idr) 8/47: Building System.FFI (System/FFI.idr) 9/47: Building System.Clock (System/Clock.idr) 10/47: Building System.Concurrency.Raw (System/Concurrency/Raw.idr) 11/47: Building Data.Bool (Data/Bool.idr) 12/47: Building Data.So (Data/So.idr) 13/47: Building System (System.idr) 14/47: Building Language.Reflection.TT (Language/Reflection/TT.idr) 15/47: Building Language.Reflection.TTImp (Language/Reflection/TTImp.idr) 16/47: Building Language.Reflection (Language/Reflection.idr) 17/47: Building Debug.Trace (Debug/Trace.idr) 18/47: Building Data.Maybe (Data/Maybe.idr) 19/47: Building Data.Either (Data/Either.idr) 20/47: Building Decidable.Equality (Decidable/Equality.idr) 21/47: Building Data.Fin (Data/Fin.idr) 22/47: Building Data.Vect (Data/Vect.idr) 23/47: Building Data.Vect.Elem (Data/Vect/Elem.idr) 24/47: Building Data.Stream (Data/Stream.idr) 25/47: Building Data.IORef (Data/IORef.idr) 26/47: Building Control.Monad.ST (Control/Monad/ST.idr) 27/47: Building Data.Ref (Data/Ref.idr) 28/47: Building Data.Primitives.Views (Data/Primitives/Views.idr) 29/47: Building Data.Morphisms (Data/Morphisms.idr) 30/47: Building Data.List.Elem (Data/List/Elem.idr) 31/47: Building Data.List.Quantifiers (Data/List/Quantifiers.idr) 32/47: Building Control.WellFounded (Control/WellFounded.idr) 33/47: Building Data.Nat.Views (Data/Nat/Views.idr) 34/47: Building Data.List.Views (Data/List/Views.idr) 35/47: Building Data.IOArray.Prims (Data/IOArray/Prims.idr) 36/47: Building Data.IOArray (Data/IOArray.idr) 37/47: Building Data.Fuel (Data/Fuel.idr) 38/47: Building Data.DPair (Data/DPair.idr) 39/47: Building System.Directory (System/Directory.idr) 40/47: Building Data.Buffer (Data/Buffer.idr) 41/47: Building Data.Bool.Xor (Data/Bool/Xor.idr) 42/47: Building Control.Monad.Identity (Control/Monad/Identity.idr) 43/47: Building Control.Monad.Trans (Control/Monad/Trans.idr) 44/47: Building Control.Monad.State (Control/Monad/State.idr) 45/47: Building Control.App (Control/App.idr) 46/47: Building Control.App.FileIO (Control/App/FileIO.idr) 47/47: Building Control.App.Console (Control/App/Console.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base' make -C libs/contrib IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' ../../build/exec/idris2 --build contrib.ipkg 1/60: Building Data.String.Extra (Data/String/Extra.idr) 2/60: Building Text.Token (Text/Token.idr) 3/60: Building Control.Delayed (Control/Delayed.idr) 4/60: Building Text.Lexer.Core (Text/Lexer/Core.idr) 5/60: Building Text.Quantity (Text/Quantity.idr) 6/60: Building Text.Lexer (Text/Lexer.idr) 7/60: Building Text.Parser.Core (Text/Parser/Core.idr) 8/60: Building Text.Parser (Text/Parser.idr) 9/60: Building System.Path (System/Path.idr) 10/60: Building System.Random (System/Random.idr) 11/60: Building Control.ANSI.CSI (Control/ANSI/CSI.idr) 12/60: Building Control.ANSI.SGR (Control/ANSI/SGR.idr) 13/60: Building Control.ANSI (Control/ANSI.idr) 14/60: Building Text.PrettyPrint.Prettyprinter.Doc (Text/PrettyPrint/Prettyprinter/Doc.idr) 15/60: Building Text.PrettyPrint.Prettyprinter.Render.Terminal (Text/PrettyPrint/Prettyprinter/Render/Terminal.idr) 16/60: Building Text.PrettyPrint.Prettyprinter.SimpleDocTree (Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr) 17/60: Building Text.PrettyPrint.Prettyprinter.Render.String (Text/PrettyPrint/Prettyprinter/Render/String.idr) 18/60: Building Text.PrettyPrint.Prettyprinter.Util (Text/PrettyPrint/Prettyprinter/Util.idr) 19/60: Building Text.PrettyPrint.Prettyprinter.Symbols (Text/PrettyPrint/Prettyprinter/Symbols.idr) 20/60: Building Text.PrettyPrint.Prettyprinter (Text/PrettyPrint/Prettyprinter.idr) 21/60: Building Language.JSON.String.Tokens (Language/JSON/String/Tokens.idr) 22/60: Building Language.JSON.String.Lexer (Language/JSON/String/Lexer.idr) 23/60: Building Language.JSON.String.Parser (Language/JSON/String/Parser.idr) 24/60: Building Language.JSON.String (Language/JSON/String.idr) 25/60: Building Language.JSON.Tokens (Language/JSON/Tokens.idr) 26/60: Building Language.JSON.Lexer (Language/JSON/Lexer.idr) 27/60: Building Language.JSON.Data (Language/JSON/Data.idr) 28/60: Building Language.JSON.Parser (Language/JSON/Parser.idr) 29/60: Building Language.JSON (Language/JSON.idr) 30/60: Building Debug.Buffer (Debug/Buffer.idr) 31/60: Building Data.Vect.Sort (Data/Vect/Sort.idr) 32/60: Building Data.String.Parser (Data/String/Parser.idr) 33/60: Building Data.String.Interpolation (Data/String/Interpolation.idr) 34/60: Building Data.SortedMap (Data/SortedMap.idr) 35/60: Building Data.SortedSet (Data/SortedSet.idr) 36/60: Building Data.Nat.Fib (Data/Nat/Fib.idr) 37/60: Building Data.Fin.Extra (Data/Fin/Extra.idr) 38/60: Building Data.Nat.Equational (Data/Nat/Equational.idr) 39/60: Building Syntax.PreorderReasoning (Syntax/PreorderReasoning.idr) 40/60: Building Data.Nat.Factor (Data/Nat/Factor.idr) 41/60: Building Data.Nat.Fact (Data/Nat/Fact.idr) 42/60: Building Data.Nat.Ack (Data/Nat/Ack.idr) 43/60: Building Control.Algebra (Control/Algebra.idr) 44/60: Building Data.Nat.Algebra (Data/Nat/Algebra.idr) 45/60: Building Data.Morphisms.Algebra (Data/Morphisms/Algebra.idr) 46/60: Building Data.Logic.Propositional (Data/Logic/Propositional.idr) 47/60: Building Data.List.Equalities (Data/List/Equalities.idr) 48/60: Building Data.List.Reverse (Data/List/Reverse.idr) 49/60: Building Data.List.Views.Extra (Data/List/Views/Extra.idr) 50/60: Building Data.List.Palindrome (Data/List/Palindrome.idr) 51/60: Building Syntax.WithProof (Syntax/WithProof.idr) 52/60: Building Data.List.TailRec (Data/List/TailRec.idr) 53/60: Building Data.List.Algebra (Data/List/Algebra.idr) 54/60: Building Data.Linear.Array (Data/Linear/Array.idr) 55/60: Building Data.Bool.Algebra (Data/Bool/Algebra.idr) 56/60: Building Control.Algebra.Implementations (Control/Algebra/Implementations.idr) 57/60: Building Control.Algebra.Laws (Control/Algebra/Laws.idr) 58/60: Building Control.Monad.Syntax (Control/Monad/Syntax.idr) 59/60: Building Control.Monad.Algebra (Control/Monad/Algebra.idr) 60/60: Building Control.Linear.LIO (Control/Linear/LIO.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib' make -C libs/network IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' ../../build/exec/idris2 --build network.ipkg 1/5: Building Network.Socket.Data (Network/Socket/Data.idr) 2/5: Building Network.FFI (Network/FFI.idr) 3/5: Building Network.Socket.Raw (Network/Socket/Raw.idr) 4/5: Building Network.Socket (Network/Socket.idr) 5/5: Building Control.Linear.Network (Control/Linear/Network.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network' make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make test INTERACTIVE='' IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.2.1/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.2.1/libs/network/build/ttc" IDRIS2_DATA=/home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/support IDRIS2_LIBS=/home/a/documents/projects/idris2/Idris2-0.2.1/bootstrap/idris2-0.2.1/lib make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.2.1/tests' ./build/exec/runtests ../../../build/exec/idris2 --only ttimp/basic001: success ttimp/basic002: success ttimp/basic003: success ttimp/basic004: success ttimp/basic005: success ttimp/basic006: success ttimp/coverage001: success ttimp/coverage002: success ttimp/dot001: success ttimp/eta001: success ttimp/eta002: success ttimp/lazy001: success ttimp/nest001: success ttimp/nest002: success ttimp/perf001: success ttimp/perf002: success ttimp/perf003: success ttimp/record001: success ttimp/record002: success ttimp/record003: success ttimp/qtt001: success ttimp/qtt003: success ttimp/total001: success ttimp/total002: success ttimp/total003: success idris2/basic001: success idris2/basic002: success idris2/basic003: success idris2/basic004: success idris2/basic005: success idris2/basic006: success idris2/basic007: success idris2/basic008: success idris2/basic009: success idris2/basic010: success idris2/basic011: success idris2/basic012: success idris2/basic013: success idris2/basic014: success idris2/basic015: success idris2/basic016: success idris2/basic017: success idris2/basic018: success idris2/basic019: success idris2/basic020: success idris2/basic021: success idris2/basic022: success idris2/basic023: success idris2/basic024: success idris2/basic025: success idris2/basic026: success idris2/basic027: success idris2/basic028: success idris2/basic029: success idris2/basic030: success idris2/basic031: success idris2/basic032: success idris2/basic033: success idris2/basic034: success idris2/basic035: success idris2/basic036: success idris2/basic037: success idris2/basic038: success idris2/basic039: success idris2/basic040: success idris2/basic041: success idris2/basic042: success idris2/coverage001: success idris2/coverage002: success idris2/coverage003: success idris2/coverage004: success idris2/coverage005: success idris2/coverage006: success idris2/coverage007: success idris2/coverage008: success idris2/coverage009: success idris2/coverage010: success idris2/docs001: success idris2/docs002: success idris2/error001: success idris2/error002: success idris2/error003: success idris2/error004: success idris2/error005: success idris2/error006: success idris2/error007: success idris2/error008: success idris2/error009: success idris2/error010: success idris2/error011: success idris2/error012: success idris2/import001: success idris2/import002: success idris2/import003: success idris2/import004: success idris2/import005: success idris2/interactive001: success idris2/interactive002: success idris2/interactive003: success idris2/interactive004: success idris2/interactive005: success idris2/interactive006: success idris2/interactive007: success idris2/interactive008: success idris2/interactive009: success idris2/interactive010: success idris2/interactive011: success idris2/interactive012: success idris2/interactive013: success idris2/interactive014: success idris2/interactive015: success idris2/interactive016: success idris2/interactive017: success idris2/interactive018: success idris2/interface001: success idris2/interface002: success idris2/interface003: success idris2/interface004: success idris2/interface005: success idris2/interface006: success idris2/interface007: success idris2/interface008: success idris2/interface009: success idris2/interface010: success idris2/interface011: success idris2/interface012: success idris2/interface013: success idris2/interface014: success idris2/interface015: success idris2/interface016: success idris2/interpreter001: success idris2/interpreter002: success idris2/interpreter003: success idris2/lazy001: success idris2/linear001: success idris2/linear002: success idris2/linear003: success idris2/linear004: success idris2/linear005: success idris2/linear006: success idris2/linear007: success idris2/linear008: success idris2/linear009: success idris2/linear010: success idris2/linear011: success idris2/linear012: success idris2/literate001: success idris2/literate002: success idris2/literate003: success idris2/literate004: success idris2/literate005: success idris2/literate006: success idris2/literate007: success idris2/literate008: success idris2/literate009: success idris2/literate010: success idris2/literate011: success idris2/literate012: success idris2/literate013: success idris2/literate014: success idris2/namespace001: success idris2/params001: success idris2/perf001: success idris2/perf002: success idris2/perf003: success idris2/perf004: success idris2/perf005: success idris2/perror001: success idris2/perror002: success idris2/perror003: success idris2/perror004: success idris2/perror005: success idris2/perror006: success idris2/pkg001: success idris2/pkg002: success idris2/pkg003: success idris2/pkg004: success idris2/pkg005: success idris2/real001: success idris2/real002: success idris2/record001: success idris2/record002: success idris2/record003: success idris2/record004: success idris2/record005: success idris2/reflection001: success idris2/reflection002: success idris2/reflection003: success idris2/reflection004: success idris2/reflection005: success idris2/reflection006: success idris2/reflection007: success idris2/reflection008: success idris2/reflection009: success idris2/reg001: success idris2/reg002: success idris2/reg003: success idris2/reg004: success idris2/reg005: success idris2/reg006: success idris2/reg007: success idris2/reg008: success idris2/reg009: success idris2/reg010: success idris2/reg011: success idris2/reg012: success idris2/reg013: success idris2/reg014: success idris2/reg015: success idris2/reg016: success idris2/reg017: success idris2/reg018: success idris2/reg019: success idris2/reg020: success idris2/reg021: success idris2/reg022: success idris2/reg023: success idris2/reg024: success idris2/reg025: success idris2/reg026: success idris2/reg027: success idris2/reg028: success idris2/reg029: success idris2/reg030: success idris2/reg031: success idris2/reg032: success idris2/reg033: success idris2/reg034: success idris2/total001: success idris2/total002: success idris2/total003: success idris2/total004: success idris2/total005: success idris2/total006: success idris2/total007: success idris2/total008: success idris2/total009: success idris2/with001: success idris2/with002: success idris2/with003: success typedd-book/chapter01: success typedd-book/chapter02: success typedd-book/chapter03: success typedd-book/chapter04: success typedd-book/chapter05: success typedd-book/chapter06: success typedd-book/chapter07: success typedd-book/chapter08: success typedd-book/chapter09: success typedd-book/chapter10: success typedd-book/chapter11: success typedd-book/chapter12: success typedd-book/chapter13: success typedd-book/chapter14: success ideMode/ideMode001: success ideMode/ideMode002: success ideMode/ideMode003: success Found Chez Scheme at /home/a/.nix-profile/bin/scheme chez/chez001: FAILURE Expected: "[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]\n1/1: Building Total (Total.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Total (Total.idr)\n[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]\nMain> Main> Bye for now!\n" chez/chez002: FAILURE Expected: "[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]\n1/1: Building Pythag (Pythag.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Pythag (Pythag.idr)\n[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]\nMain> Main> Bye for now!\n" chez/chez003: FAILURE Expected: "94\n94\n188\n188\n1/1: Building IORef (IORef.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building IORef (IORef.idr)\n94\n94\n188\n188\nMain> Main> Bye for now!\n" chez/chez004: FAILURE Expected: "100\n94\n94.42\n\"Hello\"\n\"there!\"\n65535\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n00 5E 00 00 00 41 41 41 41 00 7B 14 AE 47 E1 9A .^...AAAA.{..G..\n57 40 00 00 W@..\n\ntotal size = 20\n48 65 6C 6C 6F 20 74 68 65 72 65 21 FF FF 00 00 Hello there!....\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n\ntotal size = 80\n1/1: Building Buffer (Buffer.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Buffer (Buffer.idr)\n100\n94\n94.42\n\"Hello\"\n\"there!\"\n65535\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n00 5E 00 00 00 41 41 41 41 00 7B 14 AE 47 E1 9A .^...AAAA.{..G..\n57 40 00 00 W@..\n\ntotal size = 20\n48 65 6C 6C 6F 20 74 68 65 72 65 21 FF FF 00 00 Hello there!....\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................\n\ntotal size = 80\nMain> Main> Bye for now!\n" chez/chez005: FAILURE Expected: "(3 ** [2, 4, 6])\n1/1: Building Filter (Filter.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Filter (Filter.idr)\n(3 ** [2, 4, 6])\nMain> Main> Bye for now!\n" chez/chez006: FAILURE Expected: "\"Nat\"\n\"List of Nat\"\n\"List of Something else\"\n\"List of Something else\"\n\"List of Bool\"\n\"Int\"\n\"Something else\"\n\"List of Type\"\n\"List of Int\"\n43\n42\n1/1: Building TypeCase (TypeCase.idr)\nMain> Main> Main.strangeId is total\nMain> Main.strangeId':\nstrangeId' _\nMain> Bye for now!\n1/1: Building TypeCase2 (TypeCase2.idr)\nTypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:\nCan't match on Nat (Erased argument) at\n5\tstrangeId {a=Nat} x = x+1\n\t ^^^\n\nTypeCase2.idr:9:5--9:8:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:\nCan't match on Nat (Erased argument) at\n9\tfoo Nat = \"Nat\"\n\t ^^^\n\n" Given: "1/1: Building TypeCase (TypeCase.idr)\n\"Nat\"\n\"List of Nat\"\n\"List of Something else\"\n\"List of Something else\"\n\"List of Bool\"\n\"Int\"\n\"Something else\"\n\"List of Type\"\n\"List of Int\"\n43\n42\nMain> Main> Main.strangeId is total\nMain> Main.strangeId':\nstrangeId' _\nMain> Bye for now!\n1/1: Building TypeCase2 (TypeCase2.idr)\nTypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:\nCan't match on Nat (Erased argument) at\n5\tstrangeId {a=Nat} x = x+1\n\t ^^^\n\nTypeCase2.idr:9:5--9:8:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:\nCan't match on Nat (Erased argument) at\n9\tfoo Nat = \"Nat\"\n\t ^^^\n\n" chez/chez007: FAILURE Expected: "\"Function from Nat to Nat\"\n\"Function from Nat to Vector of 0 Int\"\n\"Function on Type\"\n1/1: Building TypeCase (TypeCase.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building TypeCase (TypeCase.idr)\n\"Function from Nat to Nat\"\n\"Function from Nat to Vector of 0 Int\"\n\"Function on Type\"\nMain> Main> Bye for now!\n" chez/chez008: FAILURE Expected: "1\n1\n1\n1/1: Building Nat (Nat.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Nat (Nat.idr)\n1\n1\n1\nMain> Main> Bye for now!\n" chez/chez009: FAILURE Expected: "42\n\228llo\n1/1: Building uni (uni.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building uni (uni.idr)\n42\n\228llo\nMain> Main> Bye for now!\n" chez/chez010: FAILURE Expected: "9\nCallback coming\nIn callback\n24\nCallback coming\nIn callback with (1, 2)\n3\n9\n'k'\n1/1: Building CB (CB.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building CB (CB.idr)\n9\nCallback coming\nIn callback\n24\nCallback coming\nIn callback with (1, 2)\n3\n9\n'k'\nMain> Main> Bye for now!\n" chez/chez011: FAILURE Expected: "5\n\"12\"\nTrue\nFalse\n1/1: Building bangs (bangs.idr)\nMain> Just 7\nMain> Just 7\nMain> Main> Main> Main> Main> Bye for now!\n" Given: "1/1: Building bangs (bangs.idr)\n5\n\"12\"\nTrue\nFalse\nMain> Just 7\nMain> Just 7\nMain> Main> Main> Main> Main> Bye for now!\n" chez/chez012: FAILURE Expected: "[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just \"Hello\", Just \"World\", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]\n[Just 1, Just 2, Just 3, Just 4, Just 5]\n1/1: Building array (array.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building array (array.idr)\n[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just \"Hello\", Just \"World\", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]\n[Just 1, Just 2, Just 3, Just 4, Just 5]\nMain> Main> Bye for now!\n" chez/chez013: FAILURE Expected: "Made it!\n(40, 30)\n\"Here\": (40, 30)\n1/1: Building Struct (Struct.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Struct (Struct.idr)\nMade it!\n(40, 30)\n\"Here\": (40, 30)\nMain> Main> Bye for now!\n" chez/chez014: FAILURE Expected: "Received: hello world!\nReceived: echo: hello world!\n1/1: Building Echo (Echo.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Echo (Echo.idr)\n[server] Failed to bind socket with error: 22\nMain> Main> Bye for now!\n" chez/chez015: FAILURE Expected: "[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]\n[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]\n1/1: Building Numbers (Numbers.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Numbers (Numbers.idr)\n[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]\n[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]\nMain> Main> Bye for now!\n" chez/chez016: FAILURE Expected: "Running Chez program located in folder with spaces\n1/1: Building Main (Main.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Main (Main.idr)\nRunning Chez program located in folder with spaces\nMain> Main> Bye for now!\n" chez/chez017: FAILURE Expected: "File Exists\nFalse\nTrue\nJust \"/home/a/documents/projects/idris2/Idris2-0.2.1/tests/chez/chez017/testdir\"\n1/1: Building dir (dir.idr)\nMain> Main> Bye for now!\nhello\n" Given: "1/1: Building dir (dir.idr)\nFile Exists\nFalse\nTrue\nJust \"/home/a/documents/projects/idris2/Idris2-0.2.1/tests/chez/chez017/testdir\"\nMain> Main> Bye for now!\nhello\n" chez/chez018: FAILURE Expected: "test test\nunfinished lineabc\ndef\nFile Not Found\n1/1: Building File (File.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building File (File.idr)\ntest test\nunfinished lineabc\ndef\nFile Not Found\nMain> Main> Bye for now!\n" chez/chez019: FAILURE Expected: "ERROR: Unhandled input for Main.foo at partial.idr:4:1--6:1\n2\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\n1/1: Building partial (partial.idr)\nMain> Main> Main> Main> Main> Bye for now!\n" Given: "1/1: Building partial (partial.idr)\nERROR: Unhandled input for Main.foo at partial.idr:4:1--6:1\n2\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\nMain> Main> Main> Main> Main> Bye for now!\n" chez/chez020: FAILURE Expected: "opened\nclosed\nIdris 2\n1/1: Building Popen (Popen.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Popen (Popen.idr)\nopened\nclosed\nIdris 2\nMain> Main> Bye for now!\n" chez/chez021: FAILURE Expected: "1\n200\nTrue\n200\n254\nFalse\n248\n1\n1234567890\n255\n65535\n4294967295\n18446744073709551615\n1/1: Building Bits (Bits.idr)\nMain> [\"1\", \"200\", \"248\", \"1\", \"255\", \"200\", \"254\"]\nMain> [\"True\", \"False\"]\nMain> [\"255\", \"65535\", \"4294967295\", \"18446744073709551615\"]\nMain> Main> Bye for now!\n" Given: "1/1: Building Bits (Bits.idr)\n1\n200\nTrue\n200\n254\nFalse\n248\n1\n1234567890\n255\n65535\n4294967295\n18446744073709551615\nMain> [\"1\", \"200\", \"248\", \"1\", \"255\", \"200\", \"254\"]\nMain> [\"True\", \"False\"]\nMain> [\"255\", \"65535\", \"4294967295\", \"18446744073709551615\"]\nMain> Main> Bye for now!\n" chez/chez022: FAILURE Expected: "Hello\nHello\nDone\nFree X\nFreeing 0 Hello\nFree Y\nFreeing 1 Hello\n1/1: Building usealloc (usealloc.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building usealloc (usealloc.idr)\nHello\nHello\nDone\nFree X\nFreeing 0 Hello\nFree Y\nFreeing 1 Hello\nMain> Main> Bye for now!\n" chez/chez023: FAILURE Expected: "Hello \n'I'\ndris!\n\nNo exceptions occurred\n1/1: Building File (File.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building File (File.idr)\nHello \n'I'\ndris!\n\nNo exceptions occurred\nMain> Main> Bye for now!\n" chez/chez024: FAILURE Expected: "True\nHI\nTrue\nHI\nTrue\nEH\nTrue\nNothing there\n1/1: Building Envy (Envy.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Envy (Envy.idr)\nTrue\nHI\nTrue\nHI\nTrue\nEH\nTrue\nNothing there\nMain> Main> Bye for now!\n" chez/chez025: FAILURE Expected: "500500\n1/1: Building runst (runst.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building runst (runst.idr)\n500500\nMain> Main> Bye for now!\n" chez/chez026: success chez/chez027: FAILURE Expected: "hiya\n2\nParse failed at position 0: satisfy\nParse failed at position 0: Not good\n['7', '6', '6', '7', '7', '5']\n['6', '3', '5', '5', '3']\n\"887\"\n\"123\"\n\"\"\nTrue\nFalse\n1/1: Building StringParser (StringParser.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building StringParser (StringParser.idr)\nhiya\n2\nParse failed at position 0: satisfy\nParse failed at position 0: Not good\n['7', '6', '6', '7', '7', '5']\n['6', '3', '5', '5', '3']\n\"887\"\n\"123\"\n\"\"\nTrue\nFalse\nMain> Main> Bye for now!\n" chez/reg001: success Found node at /usr/bin/node node/node001: FAILURE Expected: "[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]\n1/1: Building Total (Total.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Total (Total.idr)\n[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]\nMain> Main> Bye for now!\n" node/node002: FAILURE Expected: "[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]\n1/1: Building Pythag (Pythag.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Pythag (Pythag.idr)\n[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]\nMain> Main> Bye for now!\n" node/node003: FAILURE Expected: "94\n94\n188\n188\n1/1: Building IORef (IORef.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building IORef (IORef.idr)\n94\n94\n188\n188\nMain> Main> Bye for now!\n" node/node004: FAILURE Expected: "100\n94\n94.42\n\"Hello\"\n\"there!\"\n65535\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n1/1: Building Buffer (Buffer.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Buffer (Buffer.idr)\n100\n94\n94.42\n\"Hello\"\n\"there!\"\n65535\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\n[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]\nMain> Main> Bye for now!\n" node/node005: FAILURE Expected: "(3 ** [2, 4, 6])\n1/1: Building Filter (Filter.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Filter (Filter.idr)\n(3 ** [2, 4, 6])\nMain> Main> Bye for now!\n" node/node006: FAILURE Expected: "\"Nat\"\n\"List of Nat\"\n\"List of Something else\"\n\"List of Something else\"\n\"List of Bool\"\n\"Int\"\n\"Something else\"\n\"List of Type\"\n\"List of Int\"\n43\n42\n1/1: Building TypeCase (TypeCase.idr)\nMain> Main> Main.strangeId is total\nMain> Main.strangeId':\nstrangeId' _\nMain> Bye for now!\n1/1: Building TypeCase2 (TypeCase2.idr)\nTypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:\nCan't match on Nat (Erased argument) at\n5\tstrangeId {a=Nat} x = x+1\n\t ^^^\n\nTypeCase2.idr:9:5--9:8:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:\nCan't match on Nat (Erased argument) at\n9\tfoo Nat = \"Nat\"\n\t ^^^\n\n" Given: "1/1: Building TypeCase (TypeCase.idr)\n\"Nat\"\n\"List of Nat\"\n\"List of Something else\"\n\"List of Something else\"\n\"List of Bool\"\n\"Int\"\n\"Something else\"\n\"List of Type\"\n\"List of Int\"\n43\n42\nMain> Main> Main.strangeId is total\nMain> Main.strangeId':\nstrangeId' _\nMain> Bye for now!\n1/1: Building TypeCase2 (TypeCase2.idr)\nTypeCase2.idr:5:14--5:17:While processing left hand side of strangeId at TypeCase2.idr:5:1--6:1:\nCan't match on Nat (Erased argument) at\n5\tstrangeId {a=Nat} x = x+1\n\t ^^^\n\nTypeCase2.idr:9:5--9:8:While processing left hand side of foo at TypeCase2.idr:9:1--10:1:\nCan't match on Nat (Erased argument) at\n9\tfoo Nat = \"Nat\"\n\t ^^^\n\n" node/node007: FAILURE Expected: "\"Function from Nat to Nat\"\n\"Function from Nat to Vector of 0 Int\"\n\"Function on Type\"\n1/1: Building TypeCase (TypeCase.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building TypeCase (TypeCase.idr)\n\"Function from Nat to Nat\"\n\"Function from Nat to Vector of 0 Int\"\n\"Function on Type\"\nMain> Main> Bye for now!\n" node/node008: FAILURE Expected: "1\n1\n1\n1/1: Building Nat (Nat.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Nat (Nat.idr)\n1\n1\n1\nMain> Main> Bye for now!\n" node/node009: FAILURE Expected: "42\n\228llo\n1/1: Building uni (uni.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building uni (uni.idr)\n42\n\228llo\nMain> Main> Bye for now!\n" node/node011: FAILURE Expected: "5\n\"12\"\nTrue\nFalse\n1/1: Building bangs (bangs.idr)\nMain> Just 7\nMain> Just 7\nMain> Main> Main> Main> Main> Bye for now!\n" Given: "1/1: Building bangs (bangs.idr)\n5\n\"12\"\nTrue\nFalse\nMain> Just 7\nMain> Just 7\nMain> Main> Main> Main> Main> Bye for now!\n" node/node012: FAILURE Expected: "[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just \"Hello\", Just \"World\", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]\n[Just 1, Just 2, Just 3, Just 4, Just 5]\n1/1: Building array (array.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building array (array.idr)\n[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just \"Hello\", Just \"World\", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]\n[Just 1, Just 2, Just 3, Just 4, Just 5]\nMain> Main> Bye for now!\n" node/node015: FAILURE Expected: "[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]\n[8650625671965379659, 5435549321212129090, 8650625671965378905, 22945956689563340, 102]\n1/1: Building Numbers (Numbers.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building Numbers (Numbers.idr)\n[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]\n[8650625671965379659, 5435549321212129090, 8650625671965378905, 22945956689563340, 102]\nMain> Main> Bye for now!\n" node/node017: FAILURE Expected: "File Exists\nFalse\nTrue\nJust \"/home/a/documents/projects/idris2/Idris2-0.2.1/tests/node/node017/testdir\"\n1/1: Building dir (dir.idr)\nMain> Main> Bye for now!\nhello\n" Given: "1/1: Building dir (dir.idr)\nFile Exists\nFalse\nTrue\nJust \"/home/a/documents/projects/idris2/Idris2-0.2.1/tests/node/node017/testdir\"\nMain> Main> Bye for now!\nhello\n" node/node018: FAILURE Expected: "test test\nunfinished lineabc\ndef\nFile Not Found\n1/1: Building File (File.idr)\nMain> Main> Bye for now!\n" Given: "1/1: Building File (File.idr)\ntest test\nunfinished lineabc\ndef\nFile Not Found\nMain> Main> Bye for now!\n" node/node019: FAILURE Expected: "ERROR: Unhandled input for Main.foo at partial.idr:4:1--6:1\n2\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\n1/1: Building partial (partial.idr)\nMain> Main> Main> Main> Main> Bye for now!\n" Given: "1/1: Building partial (partial.idr)\nERROR: Unhandled input for Main.foo at partial.idr:4:1--6:1\n2\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\nERROR: Unhandled input for Main.lookup' at partial.idr:19:1--21:1\nMain> Main> Main> Main> Main> Bye for now!\n" node/node021: FAILURE Expected: "1\n200\nTrue\n200\n254\nFalse\n248\n1\n1234567890\n255\n65535\n4294967295\n18446744073709551615\n1/1: Building Bits (Bits.idr)\nMain> [\"1\", \"200\", \"248\", \"1\", \"255\", \"200\", \"254\"]\nMain> [\"True\", \"False\"]\nMain> [\"255\", \"65535\", \"4294967295\", \"18446744073709551615\"]\nMain> Main> Bye for now!\n" Given: "1/1: Building Bits (Bits.idr)\n1\n200\nTrue\n200\n254\nFalse\n248\n1\n1234567890\n255\n65535\n4294967295\n18446744073709551615\nMain> [\"1\", \"200\", \"248\", \"1\", \"255\", \"200\", \"254\"]\nMain> [\"True\", \"False\"]\nMain> [\"255\", \"65535\", \"4294967295\", \"18446744073709551615\"]\nMain> Main> Bye for now!\n" node/reg001: success node/syntax001: success node/tailrec001: success 262/304 tests successful make[2]: *** [Makefile:6: test] Error 1 make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1/tests' make[1]: *** [Makefile:83: test] Error 2 make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.2.1' make: *** [Makefile:166: bootstrap-test] Error 2 ```

Alternatives tried

Other information

@leahneukirchen seems to have been able to reproduce this issue and suggested that it may be caused by stdio buffering issues.

nothingnesses commented 3 years ago

Update for Idris 2 v0.3.0

These are outputs when I used the chez-scheme package from the Void Linux repositories. I also tried with the chez package from the NixOS repositories which produced essentially the same results.

Reproduction

(Click to expand) ``` $ uname -a Linux a 5.9.16_1 #1 SMP 1608571490 x86_64 GNU/Linux $ lsb_release -a LSB Version: 1.0 Distributor ID: VoidLinux Description: Void Linux Release: rolling Codename: void $ make --version GNU Make 4.3 Built for x86_64-unknown-linux-musl Copyright (C) 1988-2020 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. $ realpath --version realpath (GNU coreutils) 8.32 Copyright (C) 2020 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later . This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. Written by Padraig Brady. $ bash --version GNU bash, version 5.1.4(1)-release (x86_64-unknown-linux-musl) Copyright (C) 2020 Free Software Foundation, Inc. License GPLv3+: GNU GPL version 3 or later This is free software; you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. $ scheme --version 9.5.4 $ node --version v14.15.4 $ which scheme /usr/bin/scheme $ which idris2 which: no idris2 in (/home/a/.cargo/bin:/home/a/.npm-global/bin:/home/a/.idris2/bin:/home/a/.local/bin:/bedrock/cross/pin/bin:/bedrock/bin:/usr/local/bin:/usr/local/sbin:/usr/bin:/usr/sbin:/bin:/sbin:/usr/local/games:/usr/games:/home/a/.cargo/bin:/home/a/.npm-global/bin:/home/a/.idris2/bin:/home/a/.local/bin:/bedrock/cross/bin) $ ls ~/.idris2 "/home/a/.idris2": No such file or directory (os error 2) $ curl -O https://www.idris-lang.org/idris2-src/idris2-0.3.0.tgz % Total % Received % Xferd Average Speed Time Time Time Current Dload Upload Total Spent Left Speed 100 2741k 100 2741k 0 0 110k 0 0:00:24 0:00:24 --:--:-- 574k $ tar xf idris2-0.3.0.tgz $ export PATH="$HOME/.idris2/bin:$PATH" $ export LD_LIBRARY_PATH="$HOME/.idris2/lib:$LD_LIBRARY_PATH" $ make bootstrap SCHEME=scheme 2>&1 | tee ~/log ```

Log

These are the contents of "~/log":

(Click to expand) ``` make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' cc -Wall -fPIC -O2 -c -o getline.o getline.c cc -Wall -fPIC -O2 -c -o idris_buffer.o idris_buffer.c cc -Wall -fPIC -O2 -c -o idris_directory.o idris_directory.c cc -Wall -fPIC -O2 -c -o idris_file.o idris_file.c cc -Wall -fPIC -O2 -c -o idris_net.o idris_net.c cc -Wall -fPIC -O2 -c -o idris_support.o idris_support.c cc -Wall -fPIC -O2 -c -o idris_term.o idris_term.c ar rc libidris2_support.a getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o idris_term.o ranlib libidris2_support.a cc -shared -o libidris2_support.so getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o idris_term.o make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' cc -Wall -fPIC -O2 -c -o casts.o casts.c cc -Wall -fPIC -O2 -c -o conCaseHelper.o conCaseHelper.c cc -Wall -fPIC -O2 -c -o mathFunctions.o mathFunctions.c cc -Wall -fPIC -O2 -c -o memoryManagement.o memoryManagement.c cc -Wall -fPIC -O2 -c -o prim.o prim.c cc -Wall -fPIC -O2 -c -o runtime.o runtime.c cc -Wall -fPIC -O2 -c -o stringOps.o stringOps.c ar rc libidris2_refc.a casts.o conCaseHelper.o mathFunctions.o memoryManagement.o prim.o runtime.o stringOps.o ranlib libidris2_refc.a make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' cp support/c/libidris2_support.so bootstrap/idris2_app sed s/libidris2_support.so/libidris2_support.so/g bootstrap/idris2_app/idris2.ss > bootstrap/idris2_app/idris2-boot.ss sed -i 's|__PREFIX__|/home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss sh ./bootstrap.sh bootstrapping SCHEME=scheme IDRIS2_VERSION=0.3.0 Building idris2-boot from idris2-boot.ss compiling idris2_app/idris2-boot.ss with output to idris2_app/idris2-boot.so /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make -C libs/prelude IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' ../../build/exec/idris2 --build prelude.ipkg 1/12: Building Builtin (Builtin.idr) 2/12: Building PrimIO (PrimIO.idr) 3/12: Building Prelude.Basics (Prelude/Basics.idr) 4/12: Building Prelude.Ops (Prelude/Ops.idr) 5/12: Building Prelude.EqOrd (Prelude/EqOrd.idr) 6/12: Building Prelude.Num (Prelude/Num.idr) 7/12: Building Prelude.Interfaces (Prelude/Interfaces.idr) 8/12: Building Prelude.Uninhabited (Prelude/Uninhabited.idr) 9/12: Building Prelude.Types (Prelude/Types.idr) 10/12: Building Prelude.Show (Prelude/Show.idr) 11/12: Building Prelude.IO (Prelude/IO.idr) 12/12: Building Prelude (Prelude.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' make -C libs/base IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' ../../build/exec/idris2 --build base.ipkg 1/58: Building Data.Nat (Data/Nat.idr) 2/58: Building Data.List1 (Data/List1.idr) 3/58: Building Data.Maybe (Data/Maybe.idr) 4/58: Building Decidable.Equality.Core (Decidable/Equality/Core.idr) 5/58: Building Data.Fin (Data/Fin.idr) 6/58: Building Data.List (Data/List.idr) 7/58: Building Data.Strings (Data/Strings.idr) 8/58: Building System.Info (System/Info.idr) 9/58: Building System.File (System/File.idr) 10/58: Building System.REPL (System/REPL.idr) 11/58: Building System.FFI (System/FFI.idr) 12/58: Building System.Clock (System/Clock.idr) 13/58: Building System.Concurrency.Raw (System/Concurrency/Raw.idr) 14/58: Building Data.Bool (Data/Bool.idr) 15/58: Building Data.So (Data/So.idr) 16/58: Building System (System.idr) 17/58: Building Language.Reflection.TT (Language/Reflection/TT.idr) 18/58: Building Language.Reflection.TTImp (Language/Reflection/TTImp.idr) 19/58: Building Language.Reflection (Language/Reflection.idr) 20/58: Building Debug.Trace (Debug/Trace.idr) 21/58: Building Data.Either (Data/Either.idr) 22/58: Building Decidable.Equality (Decidable/Equality.idr) 23/58: Building Data.Vect (Data/Vect.idr) 24/58: Building Data.Vect.Quantifiers (Data/Vect/Quantifiers.idr) 25/58: Building Data.Vect.Elem (Data/Vect/Elem.idr) 26/58: Building Data.These (Data/These.idr) 27/58: Building Data.Stream (Data/Stream.idr) 28/58: Building Data.IORef (Data/IORef.idr) 29/58: Building Control.Monad.ST (Control/Monad/ST.idr) 30/58: Building Data.Ref (Data/Ref.idr) 31/58: Building Data.Primitives.Views (Data/Primitives/Views.idr) 32/58: Building Data.Morphisms (Data/Morphisms.idr) 33/58: Building Data.List.Elem (Data/List/Elem.idr) 34/58: Building Data.List.Quantifiers (Data/List/Quantifiers.idr) 35/58: Building Control.WellFounded (Control/WellFounded.idr) 36/58: Building Data.Nat.Views (Data/Nat/Views.idr) 37/58: Building Data.List.Views (Data/List/Views.idr) 38/58: Building Data.IOArray.Prims (Data/IOArray/Prims.idr) 39/58: Building Data.IOArray (Data/IOArray.idr) 40/58: Building Data.Fuel (Data/Fuel.idr) 41/58: Building Data.Fun (Data/Fun.idr) 42/58: Building Data.Rel (Data/Rel.idr) 43/58: Building Decidable.Decidable (Decidable/Decidable.idr) 44/58: Building Decidable.Order (Decidable/Order.idr) 45/58: Building Data.Nat.Order (Data/Nat/Order.idr) 46/58: Building Data.Fin.Order (Data/Fin/Order.idr) 47/58: Building Data.DPair (Data/DPair.idr) 48/58: Building System.Directory (System/Directory.idr) 49/58: Building Data.Buffer (Data/Buffer.idr) 50/58: Building Data.Bool.Xor (Data/Bool/Xor.idr) 51/58: Building Control.Monad.Trans (Control/Monad/Trans.idr) 52/58: Building Control.Monad.Identity (Control/Monad/Identity.idr) 53/58: Building Control.Monad.Reader (Control/Monad/Reader.idr) 54/58: Building Control.Monad.State (Control/Monad/State.idr) 55/58: Building Control.Monad.Either (Control/Monad/Either.idr) 56/58: Building Control.App (Control/App.idr) 57/58: Building Control.App.FileIO (Control/App/FileIO.idr) 58/58: Building Control.App.Console (Control/App/Console.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' make -C libs/contrib IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' ../../build/exec/idris2 --build contrib.ipkg 1/82: Building System.Random (System/Random.idr) 2/82: Building System.Future (System/Future.idr) 3/82: Building Control.ANSI.CSI (Control/ANSI/CSI.idr) 4/82: Building Control.ANSI.SGR (Control/ANSI/SGR.idr) 5/82: Building Control.ANSI (Control/ANSI.idr) 6/82: Building Data.String.Extra (Data/String/Extra.idr) 7/82: Building Text.PrettyPrint.Prettyprinter.Doc (Text/PrettyPrint/Prettyprinter/Doc.idr) 8/82: Building Text.PrettyPrint.Prettyprinter.Render.Terminal (Text/PrettyPrint/Prettyprinter/Render/Terminal.idr) 9/82: Building Control.Delayed (Control/Delayed.idr) 10/82: Building Text.Parser.Core (Text/Parser/Core.idr) 11/82: Building Text.Quantity (Text/Quantity.idr) 12/82: Building Text.Token (Text/Token.idr) 13/82: Building Text.Parser (Text/Parser.idr) 14/82: Building Text.PrettyPrint.Prettyprinter.SimpleDocTree (Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr) 15/82: Building Text.PrettyPrint.Prettyprinter.Render.String (Text/PrettyPrint/Prettyprinter/Render/String.idr) 16/82: Building Text.PrettyPrint.Prettyprinter.Util (Text/PrettyPrint/Prettyprinter/Util.idr) 17/82: Building Text.PrettyPrint.Prettyprinter.Symbols (Text/PrettyPrint/Prettyprinter/Symbols.idr) 18/82: Building Text.PrettyPrint.Prettyprinter (Text/PrettyPrint/Prettyprinter.idr) 19/82: Building Text.Lexer.Core (Text/Lexer/Core.idr) 20/82: Building Text.Lexer (Text/Lexer.idr) 21/82: Building System.Path (System/Path.idr) 22/82: Building Test.Golden (Test/Golden.idr) 23/82: Building Language.JSON.String.Tokens (Language/JSON/String/Tokens.idr) 24/82: Building Language.JSON.String.Lexer (Language/JSON/String/Lexer.idr) 25/82: Building Language.JSON.String.Parser (Language/JSON/String/Parser.idr) 26/82: Building Language.JSON.String (Language/JSON/String.idr) 27/82: Building Language.JSON.Tokens (Language/JSON/Tokens.idr) 28/82: Building Language.JSON.Lexer (Language/JSON/Lexer.idr) 29/82: Building Language.JSON.Data (Language/JSON/Data.idr) 30/82: Building Language.JSON.Parser (Language/JSON/Parser.idr) 31/82: Building Language.JSON (Language/JSON.idr) 32/82: Building Data.HVect (Data/HVect.idr) 33/82: Building Data.Fun.Extra (Data/Fun/Extra.idr) 34/82: Building Data.Rel.Complement (Data/Rel/Complement.idr) 35/82: Building Decidable.Decidable.Extra (Decidable/Decidable/Extra.idr) 36/82: Building Debug.Buffer (Debug/Buffer.idr) 37/82: Building Data.Vect.Sort (Data/Vect/Sort.idr) 38/82: Building Data.String.Parser (Data/String/Parser.idr) 39/82: Building Data.String.Parser.Expression (Data/String/Parser/Expression.idr) 40/82: Building Data.List.Lazy (Data/List/Lazy.idr) 41/82: Building Data.String.Iterator (Data/String/Iterator.idr) 42/82: Building Data.String.Interpolation (Data/String/Interpolation.idr) 43/82: Building Data.Stream.Extra (Data/Stream/Extra.idr) 44/82: Building Data.SortedMap (Data/SortedMap.idr) 45/82: Building Data.SortedSet (Data/SortedSet.idr) 46/82: Building Data.Late (Data/Late.idr) 47/82: Building Data.InductionRecursion.DybjerSetzer (Data/InductionRecursion/DybjerSetzer.idr) 48/82: Building Data.Recursion.Free (Data/Recursion/Free.idr) 49/82: Building Data.Nat.Fib (Data/Nat/Fib.idr) 50/82: Building Data.Fin.Extra (Data/Fin/Extra.idr) 51/82: Building Data.Nat.Equational (Data/Nat/Equational.idr) 52/82: Building Syntax.PreorderReasoning (Syntax/PreorderReasoning.idr) 53/82: Building Data.Nat.Factor (Data/Nat/Factor.idr) 54/82: Building Data.Nat.Fact (Data/Nat/Fact.idr) 55/82: Building Syntax.WithProof (Syntax/WithProof.idr) 56/82: Building Syntax.PreorderReasoning.Generic (Syntax/PreorderReasoning/Generic.idr) 57/82: Building Decidable.Order.Strict (Decidable/Order/Strict.idr) 58/82: Building Data.Nat.Order.Strict (Data/Nat/Order/Strict.idr) 59/82: Building Data.Void (Data/Void.idr) 60/82: Building Data.Bool.Decidable (Data/Bool/Decidable.idr) 61/82: Building Data.Nat.Order.Properties (Data/Nat/Order/Properties.idr) 62/82: Building Data.Nat.Properties (Data/Nat/Properties.idr) 63/82: Building Data.Nat.Division (Data/Nat/Division.idr) 64/82: Building Data.Nat.Ack (Data/Nat/Ack.idr) 65/82: Building Control.Algebra (Control/Algebra.idr) 66/82: Building Data.Nat.Algebra (Data/Nat/Algebra.idr) 67/82: Building Data.Morphisms.Algebra (Data/Morphisms/Algebra.idr) 68/82: Building Data.Logic.Propositional (Data/Logic/Propositional.idr) 69/82: Building Data.List.Equalities (Data/List/Equalities.idr) 70/82: Building Data.List.Reverse (Data/List/Reverse.idr) 71/82: Building Data.List.Views.Extra (Data/List/Views/Extra.idr) 72/82: Building Data.List.Palindrome (Data/List/Palindrome.idr) 73/82: Building Data.List.TailRec (Data/List/TailRec.idr) 74/82: Building Data.List.Algebra (Data/List/Algebra.idr) 75/82: Building Data.Linear.Array (Data/Linear/Array.idr) 76/82: Building Data.Container (Data/Container.idr) 77/82: Building Data.Bool.Algebra (Data/Bool/Algebra.idr) 78/82: Building Control.Algebra.Implementations (Control/Algebra/Implementations.idr) 79/82: Building Control.Algebra.Laws (Control/Algebra/Laws.idr) 80/82: Building Control.Monad.Syntax (Control/Monad/Syntax.idr) 81/82: Building Control.Monad.Algebra (Control/Monad/Algebra.idr) 82/82: Building Control.Linear.LIO (Control/Linear/LIO.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' make -C libs/network IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' ../../build/exec/idris2 --build network.ipkg 1/5: Building Network.Socket.Data (Network/Socket/Data.idr) 2/5: Building Network.FFI (Network/FFI.idr) 3/5: Building Network.Socket.Raw (Network/Socket/Raw.idr) 4/5: Building Network.Socket (Network/Socket.idr) 5/5: Building Control.Linear.Network (Control/Linear/Network.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0' mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/bin/ install build/exec/idris2 /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/bin mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/lib/ install support/c/libidris2_support.so /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/lib mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/bin/idris2_app install build/exec/idris2_app/* /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/bin/idris2_app mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/chez mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/racket mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/gambit mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/js install support/chez/* /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/chez install support/racket/* /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/racket install support/gambit/* /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/gambit install support/js/* /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support/js make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/lib mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/include install -m 755 libidris2_support.so /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/lib install -m 644 libidris2_support.a /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/lib install -m 644 *.h /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/include make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' mkdir -p /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/refc install libidris2_refc.a *.h /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/refc make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' make -C libs/prelude install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' ../../build/exec/idris2 --install prelude.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Builtin.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/PrimIO.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/Basics.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/EqOrd.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/Interfaces.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/IO.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/Num.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/Ops.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/Show.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/Types.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc/Prelude/Uninhabited.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/prelude/Prelude make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' make -C libs/base install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' ../../build/exec/idris2 --install base.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/App.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/App/Console.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/App Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/App/FileIO.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/App Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/Monad/Either.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/Monad/Identity.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/Monad/Reader.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/Monad/ST.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/Monad/State.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/Monad/Trans.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Control/WellFounded.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Control Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Bool.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Bool/Xor.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/Bool Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Buffer.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/DPair.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Either.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Fin.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Fin/Order.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/Fin Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Fuel.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Fun.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/IOArray.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/IOArray/Prims.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/IOArray Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/IORef.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/List.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/List/Elem.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/List/Views.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/List/Quantifiers.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/List1.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Maybe.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Morphisms.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Nat.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Nat/Order.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Nat/Views.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Primitives/Views.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/Primitives Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Ref.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Rel.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/So.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Stream.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Strings.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/These.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Vect.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Vect/Elem.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/Vect Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Data/Vect/Quantifiers.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Data/Vect Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Debug/Trace.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Debug Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Decidable/Decidable.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Decidable Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Decidable/Equality.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Decidable Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Decidable/Equality/Core.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Decidable/Equality Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Decidable/Order.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Decidable Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Language/Reflection.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Language Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Language/Reflection/TT.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Language/Reflection Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/Language/Reflection/TTImp.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/Language/Reflection Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System/Concurrency/Raw.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/System/Concurrency Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System/Clock.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System/Directory.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System/File.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System/FFI.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System/Info.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc/System/REPL.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/base/System make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' make -C libs/contrib install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' ../../build/exec/idris2 --install contrib.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/ANSI.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/ANSI/SGR.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control/ANSI Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/ANSI/CSI.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control/ANSI Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/Delayed.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/Linear/LIO.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control/Linear Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/Monad/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/Monad/Syntax.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control/Monad Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/Algebra/Laws.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control/Algebra Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Control/Algebra/Implementations.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Control/Algebra Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Bool/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Bool Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Bool/Decidable.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Bool Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Container.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Fin/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Fin Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Fun/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Fun Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/InductionRecursion/DybjerSetzer.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/InductionRecursion Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Late.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Linear/Array.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Linear Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/List/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/List/TailRec.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/List/Equalities.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/List/Reverse.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/List/Lazy.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/List/Views/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/List/Views Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/List/Palindrome.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/List Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Logic/Propositional.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Logic Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Morphisms/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Morphisms Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Algebra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Ack.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Division.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Equational.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Fact.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Factor.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Fib.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Order/Strict.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat/Order Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Order/Properties.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat/Order Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Nat/Properties.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Nat Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Recursion/Free.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Recursion Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/SortedMap.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/SortedSet.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Stream/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Stream Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/String/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/String Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/String/Interpolation.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/String Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/String/Iterator.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/String Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/String/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/String Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/String/Parser/Expression.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/String/Parser Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Vect/Sort.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data/Vect Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/Void.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Data/HVect.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Data Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Debug/Buffer.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Debug Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Decidable/Order/Strict.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Decidable/Order Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Decidable/Decidable/Extra.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Decidable/Decidable Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/Data.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/Lexer.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/String.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/String/Lexer.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON/String Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/String/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON/String Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/String/Tokens.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON/String Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Language/JSON/Tokens.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Language/JSON Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Test/Golden.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Test Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/Token.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/Quantity.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/Parser.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/Lexer.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/Parser/Core.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/Parser Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/Lexer/Core.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/Lexer Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/PrettyPrint Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Doc.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Symbols.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Util.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/SimpleDocTree.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/PrettyPrint/Prettyprinter Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Render/String.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/PrettyPrint/Prettyprinter/Render Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Text/PrettyPrint/Prettyprinter/Render/Terminal.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Text/PrettyPrint/Prettyprinter/Render Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/System/Future.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/System/Random.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/System/Path.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/System Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Syntax/WithProof.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Syntax Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Syntax/PreorderReasoning.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Syntax Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc/Syntax/PreorderReasoning/Generic.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/contrib/Syntax/PreorderReasoning make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' make -C libs/network install IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' ../../build/exec/idris2 --install network.ipkg Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc/Control/Linear/Network.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/network/Control/Linear Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc/Network/Socket.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/network/Network Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc/Network/Socket/Data.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/network/Network/Socket Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc/Network/Socket/Raw.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/network/Network/Socket Installing /home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc/Network/FFI.ttc to /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/network/Network make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make -C libs/prelude clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' make -C libs/base clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' make -C libs/contrib clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' make -C libs/network clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' rm -f getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o idris_term.o libidris2_support.so libidris2_support.a make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' rm -f casts.o conCaseHelper.o mathFunctions.o memoryManagement.o prim.o runtime.o stringOps.o libidris2_refc.a make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/bin/idris2 --clean idris2.ipkg Removed: /home/a/documents/projects/idris2/Idris2-0.3.0/build/exec/idris2 rm -f src/IdrisPaths.idr make -C tests clean make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/tests' rm -f -r build make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/tests' rm -f -r build make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' cc -Wall -fPIC -O2 -c -o getline.o getline.c cc -Wall -fPIC -O2 -c -o idris_buffer.o idris_buffer.c cc -Wall -fPIC -O2 -c -o idris_directory.o idris_directory.c cc -Wall -fPIC -O2 -c -o idris_file.o idris_file.c cc -Wall -fPIC -O2 -c -o idris_net.o idris_net.c cc -Wall -fPIC -O2 -c -o idris_support.o idris_support.c cc -Wall -fPIC -O2 -c -o idris_term.o idris_term.c ar rc libidris2_support.a getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o idris_term.o ranlib libidris2_support.a cc -shared -o libidris2_support.so getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o idris_term.o make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/c' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' cc -Wall -fPIC -O2 -c -o casts.o casts.c cc -Wall -fPIC -O2 -c -o conCaseHelper.o conCaseHelper.c cc -Wall -fPIC -O2 -c -o mathFunctions.o mathFunctions.c cc -Wall -fPIC -O2 -c -o memoryManagement.o memoryManagement.c cc -Wall -fPIC -O2 -c -o prim.o prim.c cc -Wall -fPIC -O2 -c -o runtime.o runtime.c cc -Wall -fPIC -O2 -c -o stringOps.o stringOps.c ar rc libidris2_refc.a casts.o conCaseHelper.o mathFunctions.o memoryManagement.o prim.o runtime.o stringOps.o ranlib libidris2_refc.a make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/support/refc' echo 'module IdrisPaths' > src/IdrisPaths.idr echo 'export idrisVersion : ((Nat,Nat,Nat), String); idrisVersion = ((0,3,0), "")' >> src/IdrisPaths.idr echo 'export yprefix : String; yprefix="/home/a/.idris2"' >> src/IdrisPaths.idr /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/bin/idris2 --build idris2.ipkg 1/162: Building Text.Bounded (src/Text/Bounded.idr) 2/162: Building Core.FC (src/Core/FC.idr) 3/162: Building Core.Name.Namespace (src/Core/Name/Namespace.idr) 4/162: Building Core.Name (src/Core/Name.idr) 5/162: Building Data.Bool.Extra (src/Data/Bool/Extra.idr) 6/162: Building Data.NameMap (src/Data/NameMap.idr) 7/162: Building Algebra.Semiring (src/Algebra/Semiring.idr) 8/162: Building Algebra.Preorder (src/Algebra/Preorder.idr) 9/162: Building Algebra.ZeroOneOmega (src/Algebra/ZeroOneOmega.idr) 10/162: Building Algebra (src/Algebra.idr) 11/162: Building Core.TT (src/Core/TT.idr) 12/162: Building Core.CompileExpr (src/Core/CompileExpr.idr) 13/162: Building Core.CaseTree (src/Core/CaseTree.idr) 14/162: Building Core.Env (src/Core/Env.idr) 15/162: Building Text.Lexer.Core (src/Text/Lexer/Core.idr) 16/162: Building Text.Quantity (src/Text/Quantity.idr) 17/162: Building Text.Token (src/Text/Token.idr) 18/162: Building Text.Lexer (src/Text/Lexer.idr) 19/162: Building Parser.Lexer.Common (src/Parser/Lexer/Common.idr) 20/162: Building Utils.Hex (src/Utils/Hex.idr) 21/162: Building Utils.Octal (src/Utils/Octal.idr) 22/162: Building Utils.String (src/Utils/String.idr) 23/162: Building Parser.Lexer.Source (src/Parser/Lexer/Source.idr) 24/162: Building Text.Parser.Core (src/Text/Parser/Core.idr) 25/162: Building Text.Parser (src/Text/Parser.idr) 26/162: Building Parser.Rule.Common (src/Parser/Rule/Common.idr) 27/162: Building Text.Literate (src/Text/Literate.idr) 28/162: Building Parser.Unlit (src/Parser/Unlit.idr) 29/162: Building Parser.Support (src/Parser/Support.idr) 30/162: Building Parser.Rule.Source (src/Parser/Rule/Source.idr) 31/162: Building Utils.Either (src/Utils/Either.idr) 32/162: Building Parser.Source (src/Parser/Source.idr) 33/162: Building Core.Core (src/Core/Core.idr) 34/162: Building Core.Hash (src/Core/Hash.idr) 35/162: Building Data.StringMap (src/Data/StringMap.idr) 36/162: Building Data.StringTrie (src/Data/StringTrie.idr) 37/162: Building Core.Options.Log (src/Core/Options/Log.idr) 38/162: Building Utils.Binary (src/Utils/Binary.idr) 39/162: Building Utils.Path (src/Utils/Path.idr) 40/162: Building Core.Options (src/Core/Options.idr) 41/162: Building Data.IntMap (src/Data/IntMap.idr) 42/162: Building Core.Context (src/Core/Context.idr) 43/162: Building Compiler.LambdaLift (src/Compiler/LambdaLift.idr) 44/162: Building Compiler.ANF (src/Compiler/ANF.idr) 45/162: Building Core.Context.Log (src/Core/Context/Log.idr) 46/162: Building Core.Value (src/Core/Value.idr) 47/162: Building Core.Primitives (src/Core/Primitives.idr) 48/162: Building Core.Normalise (src/Core/Normalise.idr) 49/162: Building Compiler.CompileExpr (src/Compiler/CompileExpr.idr) 50/162: Building Data.LengthMatch (src/Data/LengthMatch.idr) 51/162: Building Compiler.Inline (src/Compiler/Inline.idr) 52/162: Building Compiler.VMCode (src/Compiler/VMCode.idr) 53/162: Building Core.Directory (src/Core/Directory.idr) 54/162: Building Core.TTC (src/Core/TTC.idr) 55/162: Building Compiler.Common (src/Compiler/Common.idr) 56/162: Building Core.InitPrimitives (src/Core/InitPrimitives.idr) 57/162: Building Core.UnifyState (src/Core/UnifyState.idr) 58/162: Building Core.Binary (src/Core/Binary.idr) 59/162: Building Core.Metadata (src/Core/Metadata.idr) 60/162: Building Core.GetType (src/Core/GetType.idr) 61/162: Building Core.Unify (src/Core/Unify.idr) 62/162: Building IdrisPaths (src/IdrisPaths.idr) 63/162: Building Idris.Version (src/Idris/Version.idr) 64/162: Building Idris.CommandLine (src/Idris/CommandLine.idr) 65/162: Building Compiler.Scheme.Common (src/Compiler/Scheme/Common.idr) 66/162: Building Compiler.Scheme.Chez (src/Compiler/Scheme/Chez.idr) 67/162: Building Compiler.Scheme.Racket (src/Compiler/Scheme/Racket.idr) 68/162: Building Compiler.Scheme.Gambit (src/Compiler/Scheme/Gambit.idr) 69/162: Building Core.AutoSearch (src/Core/AutoSearch.idr) 70/162: Building Data.ANameMap (src/Data/ANameMap.idr) 71/162: Building TTImp.TTImp (src/TTImp/TTImp.idr) 72/162: Building Idris.Syntax (src/Idris/Syntax.idr) 73/162: Building TTImp.Utils (src/TTImp/Utils.idr) 74/162: Building TTImp.Unelab (src/TTImp/Unelab.idr) 75/162: Building Idris.Resugar (src/Idris/Resugar.idr) 76/162: Building Idris.DocString (src/Idris/DocString.idr) 77/162: Building TTImp.BindImplicits (src/TTImp/BindImplicits.idr) 78/162: Building Core.LinearCheck (src/Core/LinearCheck.idr) 79/162: Building TTImp.Elab.Check (src/TTImp/Elab/Check.idr) 80/162: Building TTImp.Elab.Delayed (src/TTImp/Elab/Delayed.idr) 81/162: Building Core.Reflect (src/Core/Reflect.idr) 82/162: Building TTImp.Elab.Ambiguity (src/TTImp/Elab/Ambiguity.idr) 83/162: Building TTImp.Elab.App (src/TTImp/Elab/App.idr) 84/162: Building TTImp.Elab.ImplicitBind (src/TTImp/Elab/ImplicitBind.idr) 85/162: Building TTImp.Elab.As (src/TTImp/Elab/As.idr) 86/162: Building TTImp.Elab.Binders (src/TTImp/Elab/Binders.idr) 87/162: Building TTImp.Elab.Case (src/TTImp/Elab/Case.idr) 88/162: Building TTImp.Elab.Dot (src/TTImp/Elab/Dot.idr) 89/162: Building TTImp.Elab.Hole (src/TTImp/Elab/Hole.idr) 90/162: Building TTImp.Elab.Lazy (src/TTImp/Elab/Lazy.idr) 91/162: Building TTImp.Elab.Utils (src/TTImp/Elab/Utils.idr) 92/162: Building TTImp.Elab.Local (src/TTImp/Elab/Local.idr) 93/162: Building TTImp.Elab.Prim (src/TTImp/Elab/Prim.idr) 94/162: Building TTImp.Reflect (src/TTImp/Reflect.idr) 95/162: Building TTImp.Elab.Quote (src/TTImp/Elab/Quote.idr) 96/162: Building TTImp.Elab.Record (src/TTImp/Elab/Record.idr) 97/162: Building TTImp.Elab.Rewrite (src/TTImp/Elab/Rewrite.idr) 98/162: Building TTImp.Elab.RunElab (src/TTImp/Elab/RunElab.idr) 99/162: Building TTImp.Elab.Term (src/TTImp/Elab/Term.idr) 100/162: Building TTImp.Elab (src/TTImp/Elab.idr) 101/162: Building Core.Termination (src/Core/Termination.idr) 102/162: Building TTImp.Parser (src/TTImp/Parser.idr) 103/162: Building Core.Context.Data (src/Core/Context/Data.idr) 104/162: Building TTImp.ProcessData (src/TTImp/ProcessData.idr) 105/162: Building Core.CaseBuilder (src/Core/CaseBuilder.idr) 106/162: Building Core.Coverage (src/Core/Coverage.idr) 107/162: Building Core.Transform (src/Core/Transform.idr) 108/162: Building TTImp.Impossible (src/TTImp/Impossible.idr) 109/162: Building TTImp.PartialEval (src/TTImp/PartialEval.idr) 110/162: Building TTImp.WithClause (src/TTImp/WithClause.idr) 111/162: Building TTImp.ProcessDef (src/TTImp/ProcessDef.idr) 112/162: Building TTImp.ProcessParams (src/TTImp/ProcessParams.idr) 113/162: Building TTImp.ProcessRecord (src/TTImp/ProcessRecord.idr) 114/162: Building TTImp.ProcessRunElab (src/TTImp/ProcessRunElab.idr) 115/162: Building TTImp.ProcessTransform (src/TTImp/ProcessTransform.idr) 116/162: Building TTImp.ProcessType (src/TTImp/ProcessType.idr) 117/162: Building TTImp.ProcessDecls (src/TTImp/ProcessDecls.idr) 118/162: Building Idris.Elab.Implementation (src/Idris/Elab/Implementation.idr) 119/162: Building Idris.Elab.Interface (src/Idris/Elab/Interface.idr) 120/162: Building Utils.Shunting (src/Utils/Shunting.idr) 121/162: Building Idris.Desugar (src/Idris/Desugar.idr) 122/162: Building TTImp.Interactive.CaseSplit (src/TTImp/Interactive/CaseSplit.idr) 123/162: Building TTImp.Interactive.ExprSearch (src/TTImp/Interactive/ExprSearch.idr) 124/162: Building Idris.REPLOpts (src/Idris/REPLOpts.idr) 125/162: Building Utils.Term (src/Utils/Term.idr) 126/162: Building Idris.Pretty (src/Idris/Pretty.idr) 127/162: Building Data.List.Extra (src/Data/List/Extra.idr) 128/162: Building Idris.Error (src/Idris/Error.idr) 129/162: Building Idris.Parser.Let (src/Idris/Parser/Let.idr) 130/162: Building Idris.Parser (src/Idris/Parser.idr) 131/162: Building Idris.IDEMode.Commands (src/Idris/IDEMode/Commands.idr) 132/162: Building Idris.REPLCommon (src/Idris/REPLCommon.idr) 133/162: Building Idris.ProcessIdr (src/Idris/ProcessIdr.idr) 134/162: Building Idris.ModTree (src/Idris/ModTree.idr) 135/162: Building Parser.Lexer.Package (src/Parser/Lexer/Package.idr) 136/162: Building Parser.Rule.Package (src/Parser/Rule/Package.idr) 137/162: Building Parser.Package (src/Parser/Package.idr) 138/162: Building Compiler.ES.ImperativeAst (src/Compiler/ES/ImperativeAst.idr) 139/162: Building Compiler.ES.RemoveUnused (src/Compiler/ES/RemoveUnused.idr) 140/162: Building Compiler.ES.TailRec (src/Compiler/ES/TailRec.idr) 141/162: Building Compiler.ES.Imperative (src/Compiler/ES/Imperative.idr) 142/162: Building Compiler.ES.ES (src/Compiler/ES/ES.idr) 143/162: Building Compiler.ES.Node (src/Compiler/ES/Node.idr) 144/162: Building Compiler.ES.Javascript (src/Compiler/ES/Javascript.idr) 145/162: Building Data.DList (src/Data/DList.idr) 146/162: Building Compiler.RefC.RefC (src/Compiler/RefC/RefC.idr) 147/162: Building Idris.IDEMode.TokenLine (src/Idris/IDEMode/TokenLine.idr) 148/162: Building Idris.IDEMode.CaseSplit (src/Idris/IDEMode/CaseSplit.idr) 149/162: Building Idris.IDEMode.MakeClause (src/Idris/IDEMode/MakeClause.idr) 150/162: Building Idris.IDEMode.Holes (src/Idris/IDEMode/Holes.idr) 151/162: Building TTImp.Interactive.GenerateDef (src/TTImp/Interactive/GenerateDef.idr) 152/162: Building TTImp.Interactive.MakeLemma (src/TTImp/Interactive/MakeLemma.idr) 153/162: Building Idris.REPL (src/Idris/REPL.idr) 154/162: Building Idris.SetOptions (src/Idris/SetOptions.idr) 155/162: Building Idris.Package (src/Idris/Package.idr) 156/162: Building Idris.IDEMode.Parser (src/Idris/IDEMode/Parser.idr) 157/162: Building Idris.IDEMode.SyntaxHighlight (src/Idris/IDEMode/SyntaxHighlight.idr) 158/162: Building Idris.IDEMode.REPL (src/Idris/IDEMode/REPL.idr) 159/162: Building Yaffle.REPL (src/Yaffle/REPL.idr) 160/162: Building Yaffle.Main (src/Yaffle/Main.idr) 161/162: Building Idris.Driver (src/Idris/Driver.idr) 162/162: Building Idris.Main (src/Idris/Main.idr) make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/tests' /home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/bin/idris2 --build tests.ipkg 1/2: Building Lib (Lib.idr) 2/2: Building Main (Main.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/tests' make -C libs/prelude IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' ../../build/exec/idris2 --build prelude.ipkg 1/12: Building Builtin (Builtin.idr) 2/12: Building PrimIO (PrimIO.idr) 3/12: Building Prelude.Basics (Prelude/Basics.idr) 4/12: Building Prelude.Ops (Prelude/Ops.idr) 5/12: Building Prelude.EqOrd (Prelude/EqOrd.idr) 6/12: Building Prelude.Num (Prelude/Num.idr) 7/12: Building Prelude.Interfaces (Prelude/Interfaces.idr) 8/12: Building Prelude.Uninhabited (Prelude/Uninhabited.idr) 9/12: Building Prelude.Types (Prelude/Types.idr) 10/12: Building Prelude.Show (Prelude/Show.idr) 11/12: Building Prelude.IO (Prelude/IO.idr) 12/12: Building Prelude (Prelude.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude' make -C libs/base IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' ../../build/exec/idris2 --build base.ipkg 1/58: Building Data.Nat (Data/Nat.idr) 2/58: Building Data.List1 (Data/List1.idr) 3/58: Building Data.Maybe (Data/Maybe.idr) 4/58: Building Decidable.Equality.Core (Decidable/Equality/Core.idr) 5/58: Building Data.Fin (Data/Fin.idr) 6/58: Building Data.List (Data/List.idr) 7/58: Building Data.Strings (Data/Strings.idr) 8/58: Building System.Info (System/Info.idr) 9/58: Building System.File (System/File.idr) 10/58: Building System.REPL (System/REPL.idr) 11/58: Building System.FFI (System/FFI.idr) 12/58: Building System.Clock (System/Clock.idr) 13/58: Building System.Concurrency.Raw (System/Concurrency/Raw.idr) 14/58: Building Data.Bool (Data/Bool.idr) 15/58: Building Data.So (Data/So.idr) 16/58: Building System (System.idr) 17/58: Building Language.Reflection.TT (Language/Reflection/TT.idr) 18/58: Building Language.Reflection.TTImp (Language/Reflection/TTImp.idr) 19/58: Building Language.Reflection (Language/Reflection.idr) 20/58: Building Debug.Trace (Debug/Trace.idr) 21/58: Building Data.Either (Data/Either.idr) 22/58: Building Decidable.Equality (Decidable/Equality.idr) 23/58: Building Data.Vect (Data/Vect.idr) 24/58: Building Data.Vect.Quantifiers (Data/Vect/Quantifiers.idr) 25/58: Building Data.Vect.Elem (Data/Vect/Elem.idr) 26/58: Building Data.These (Data/These.idr) 27/58: Building Data.Stream (Data/Stream.idr) 28/58: Building Data.IORef (Data/IORef.idr) 29/58: Building Control.Monad.ST (Control/Monad/ST.idr) 30/58: Building Data.Ref (Data/Ref.idr) 31/58: Building Data.Primitives.Views (Data/Primitives/Views.idr) 32/58: Building Data.Morphisms (Data/Morphisms.idr) 33/58: Building Data.List.Elem (Data/List/Elem.idr) 34/58: Building Data.List.Quantifiers (Data/List/Quantifiers.idr) 35/58: Building Control.WellFounded (Control/WellFounded.idr) 36/58: Building Data.Nat.Views (Data/Nat/Views.idr) 37/58: Building Data.List.Views (Data/List/Views.idr) 38/58: Building Data.IOArray.Prims (Data/IOArray/Prims.idr) 39/58: Building Data.IOArray (Data/IOArray.idr) 40/58: Building Data.Fuel (Data/Fuel.idr) 41/58: Building Data.Fun (Data/Fun.idr) 42/58: Building Data.Rel (Data/Rel.idr) 43/58: Building Decidable.Decidable (Decidable/Decidable.idr) 44/58: Building Decidable.Order (Decidable/Order.idr) 45/58: Building Data.Nat.Order (Data/Nat/Order.idr) 46/58: Building Data.Fin.Order (Data/Fin/Order.idr) 47/58: Building Data.DPair (Data/DPair.idr) 48/58: Building System.Directory (System/Directory.idr) 49/58: Building Data.Buffer (Data/Buffer.idr) 50/58: Building Data.Bool.Xor (Data/Bool/Xor.idr) 51/58: Building Control.Monad.Trans (Control/Monad/Trans.idr) 52/58: Building Control.Monad.Identity (Control/Monad/Identity.idr) 53/58: Building Control.Monad.Reader (Control/Monad/Reader.idr) 54/58: Building Control.Monad.State (Control/Monad/State.idr) 55/58: Building Control.Monad.Either (Control/Monad/Either.idr) 56/58: Building Control.App (Control/App.idr) 57/58: Building Control.App.FileIO (Control/App/FileIO.idr) 58/58: Building Control.App.Console (Control/App/Console.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base' make -C libs/contrib IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' ../../build/exec/idris2 --build contrib.ipkg 1/82: Building System.Random (System/Random.idr) 2/82: Building System.Future (System/Future.idr) 3/82: Building Control.ANSI.CSI (Control/ANSI/CSI.idr) 4/82: Building Control.ANSI.SGR (Control/ANSI/SGR.idr) 5/82: Building Control.ANSI (Control/ANSI.idr) 6/82: Building Data.String.Extra (Data/String/Extra.idr) 7/82: Building Text.PrettyPrint.Prettyprinter.Doc (Text/PrettyPrint/Prettyprinter/Doc.idr) 8/82: Building Text.PrettyPrint.Prettyprinter.Render.Terminal (Text/PrettyPrint/Prettyprinter/Render/Terminal.idr) 9/82: Building Control.Delayed (Control/Delayed.idr) 10/82: Building Text.Parser.Core (Text/Parser/Core.idr) 11/82: Building Text.Quantity (Text/Quantity.idr) 12/82: Building Text.Token (Text/Token.idr) 13/82: Building Text.Parser (Text/Parser.idr) 14/82: Building Text.PrettyPrint.Prettyprinter.SimpleDocTree (Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr) 15/82: Building Text.PrettyPrint.Prettyprinter.Render.String (Text/PrettyPrint/Prettyprinter/Render/String.idr) 16/82: Building Text.PrettyPrint.Prettyprinter.Util (Text/PrettyPrint/Prettyprinter/Util.idr) 17/82: Building Text.PrettyPrint.Prettyprinter.Symbols (Text/PrettyPrint/Prettyprinter/Symbols.idr) 18/82: Building Text.PrettyPrint.Prettyprinter (Text/PrettyPrint/Prettyprinter.idr) 19/82: Building Text.Lexer.Core (Text/Lexer/Core.idr) 20/82: Building Text.Lexer (Text/Lexer.idr) 21/82: Building System.Path (System/Path.idr) 22/82: Building Test.Golden (Test/Golden.idr) 23/82: Building Language.JSON.String.Tokens (Language/JSON/String/Tokens.idr) 24/82: Building Language.JSON.String.Lexer (Language/JSON/String/Lexer.idr) 25/82: Building Language.JSON.String.Parser (Language/JSON/String/Parser.idr) 26/82: Building Language.JSON.String (Language/JSON/String.idr) 27/82: Building Language.JSON.Tokens (Language/JSON/Tokens.idr) 28/82: Building Language.JSON.Lexer (Language/JSON/Lexer.idr) 29/82: Building Language.JSON.Data (Language/JSON/Data.idr) 30/82: Building Language.JSON.Parser (Language/JSON/Parser.idr) 31/82: Building Language.JSON (Language/JSON.idr) 32/82: Building Data.HVect (Data/HVect.idr) 33/82: Building Data.Fun.Extra (Data/Fun/Extra.idr) 34/82: Building Data.Rel.Complement (Data/Rel/Complement.idr) 35/82: Building Decidable.Decidable.Extra (Decidable/Decidable/Extra.idr) 36/82: Building Debug.Buffer (Debug/Buffer.idr) 37/82: Building Data.Vect.Sort (Data/Vect/Sort.idr) 38/82: Building Data.String.Parser (Data/String/Parser.idr) 39/82: Building Data.String.Parser.Expression (Data/String/Parser/Expression.idr) 40/82: Building Data.List.Lazy (Data/List/Lazy.idr) 41/82: Building Data.String.Iterator (Data/String/Iterator.idr) 42/82: Building Data.String.Interpolation (Data/String/Interpolation.idr) 43/82: Building Data.Stream.Extra (Data/Stream/Extra.idr) 44/82: Building Data.SortedMap (Data/SortedMap.idr) 45/82: Building Data.SortedSet (Data/SortedSet.idr) 46/82: Building Data.Late (Data/Late.idr) 47/82: Building Data.InductionRecursion.DybjerSetzer (Data/InductionRecursion/DybjerSetzer.idr) 48/82: Building Data.Recursion.Free (Data/Recursion/Free.idr) 49/82: Building Data.Nat.Fib (Data/Nat/Fib.idr) 50/82: Building Data.Fin.Extra (Data/Fin/Extra.idr) 51/82: Building Data.Nat.Equational (Data/Nat/Equational.idr) 52/82: Building Syntax.PreorderReasoning (Syntax/PreorderReasoning.idr) 53/82: Building Data.Nat.Factor (Data/Nat/Factor.idr) 54/82: Building Data.Nat.Fact (Data/Nat/Fact.idr) 55/82: Building Syntax.WithProof (Syntax/WithProof.idr) 56/82: Building Syntax.PreorderReasoning.Generic (Syntax/PreorderReasoning/Generic.idr) 57/82: Building Decidable.Order.Strict (Decidable/Order/Strict.idr) 58/82: Building Data.Nat.Order.Strict (Data/Nat/Order/Strict.idr) 59/82: Building Data.Void (Data/Void.idr) 60/82: Building Data.Bool.Decidable (Data/Bool/Decidable.idr) 61/82: Building Data.Nat.Order.Properties (Data/Nat/Order/Properties.idr) 62/82: Building Data.Nat.Properties (Data/Nat/Properties.idr) 63/82: Building Data.Nat.Division (Data/Nat/Division.idr) 64/82: Building Data.Nat.Ack (Data/Nat/Ack.idr) 65/82: Building Control.Algebra (Control/Algebra.idr) 66/82: Building Data.Nat.Algebra (Data/Nat/Algebra.idr) 67/82: Building Data.Morphisms.Algebra (Data/Morphisms/Algebra.idr) 68/82: Building Data.Logic.Propositional (Data/Logic/Propositional.idr) 69/82: Building Data.List.Equalities (Data/List/Equalities.idr) 70/82: Building Data.List.Reverse (Data/List/Reverse.idr) 71/82: Building Data.List.Views.Extra (Data/List/Views/Extra.idr) 72/82: Building Data.List.Palindrome (Data/List/Palindrome.idr) 73/82: Building Data.List.TailRec (Data/List/TailRec.idr) 74/82: Building Data.List.Algebra (Data/List/Algebra.idr) 75/82: Building Data.Linear.Array (Data/Linear/Array.idr) 76/82: Building Data.Container (Data/Container.idr) 77/82: Building Data.Bool.Algebra (Data/Bool/Algebra.idr) 78/82: Building Control.Algebra.Implementations (Control/Algebra/Implementations.idr) 79/82: Building Control.Algebra.Laws (Control/Algebra/Laws.idr) 80/82: Building Control.Monad.Syntax (Control/Monad/Syntax.idr) 81/82: Building Control.Monad.Algebra (Control/Monad/Algebra.idr) 82/82: Building Control.Linear.LIO (Control/Linear/LIO.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib' make -C libs/network IDRIS2=../../build/exec/idris2 IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' ../../build/exec/idris2 --build network.ipkg 1/5: Building Network.Socket.Data (Network/Socket/Data.idr) 2/5: Building Network.FFI (Network/FFI.idr) 3/5: Building Network.Socket.Raw (Network/Socket/Raw.idr) 4/5: Building Network.Socket (Network/Socket.idr) 5/5: Building Control.Linear.Network (Control/Linear/Network.idr) make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network' make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make test INTERACTIVE='' IDRIS2_PATH="/home/a/documents/projects/idris2/Idris2-0.3.0/libs/prelude/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/base/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/contrib/build/ttc:/home/a/documents/projects/idris2/Idris2-0.3.0/libs/network/build/ttc" IDRIS2_DATA=/home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/support IDRIS2_LIBS=/home/a/documents/projects/idris2/Idris2-0.3.0/bootstrap/idris2-0.3.0/lib make[1]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make[2]: Entering directory '/home/a/documents/projects/idris2/Idris2-0.3.0/tests' ./build/exec/runtests ../../../build/exec/idris2 --only ttimp/basic001: success ttimp/basic002: success ttimp/basic003: success ttimp/basic004: success ttimp/basic005: success ttimp/basic006: success ttimp/coverage001: success ttimp/coverage002: success ttimp/dot001: success ttimp/eta001: success ttimp/eta002: success ttimp/lazy001: success ttimp/nest001: success ttimp/nest002: success ttimp/perf001: success ttimp/perf002: success ttimp/perf003: success ttimp/record001: success ttimp/record002: success ttimp/record003: success ttimp/qtt001: success ttimp/qtt003: success ttimp/total001: success ttimp/total002: success ttimp/total003: success idris2/basic001: success idris2/basic002: success idris2/basic003: success idris2/basic004: success idris2/basic005: success idris2/basic006: success idris2/basic007: success idris2/basic008: success idris2/basic009: success idris2/basic010: success idris2/basic011: success idris2/basic012: success idris2/basic013: success idris2/basic014: success idris2/basic015: success idris2/basic016: success idris2/basic017: success idris2/basic018: success idris2/basic019: success idris2/basic020: success idris2/basic021: success idris2/basic022: success idris2/basic023: success idris2/basic024: success idris2/basic025: success idris2/basic026: success idris2/basic027: success idris2/basic028: success idris2/basic029: success idris2/basic030: success idris2/basic031: success idris2/basic032: success idris2/basic033: success idris2/basic034: success idris2/basic035: success idris2/basic036: success idris2/basic037: success idris2/basic038: success idris2/basic039: success idris2/basic040: success idris2/basic041: success idris2/basic042: success idris2/basic043: success idris2/basic044: success idris2/basic045: success idris2/basic046: success idris2/basic047: success idris2/basic048: success idris2/basic049: success idris2/basic050: success idris2/basic051: success idris2/coverage001: success idris2/coverage002: success idris2/coverage003: success idris2/coverage004: success idris2/coverage005: success idris2/coverage006: success idris2/coverage007: success idris2/coverage008: success idris2/coverage009: success idris2/coverage010: success idris2/coverage011: success idris2/docs001: success idris2/docs002: success idris2/evaluator001: success idris2/evaluator002: success idris2/evaluator003: success idris2/evaluator004: success idris2/error001: success idris2/error002: success idris2/error003: success idris2/error004: success idris2/error005: success idris2/error006: success idris2/error007: success idris2/error008: success idris2/error009: success idris2/error010: success idris2/error011: success idris2/error012: success idris2/error013: success idris2/error014: success idris2/import001: success idris2/import002: success idris2/import003: success idris2/import004: success idris2/import005: success idris2/interactive001: success idris2/interactive002: success idris2/interactive003: success idris2/interactive004: success idris2/interactive005: success idris2/interactive006: success idris2/interactive007: success idris2/interactive008: success idris2/interactive009: success idris2/interactive010: success idris2/interactive011: success idris2/interactive012: success idris2/interactive013: success idris2/interactive014: success idris2/interactive015: success idris2/interactive016: success idris2/interactive017: success idris2/interactive018: success idris2/interface001: success idris2/interface002: success idris2/interface003: success idris2/interface004: success idris2/interface005: success idris2/interface006: success idris2/interface007: success idris2/interface008: success idris2/interface009: success idris2/interface010: success idris2/interface011: success idris2/interface012: success idris2/interface013: success idris2/interface014: success idris2/interface015: success idris2/interface016: success idris2/interface017: success idris2/interface018: success idris2/interface019: success idris2/interface020: success idris2/interface021: success idris2/interpreter001: success idris2/interpreter002: success idris2/interpreter003: success idris2/interpreter004: success idris2/interpreter005: success idris2/interpreter006: success idris2/lazy001: success idris2/linear001: success idris2/linear002: success idris2/linear003: success idris2/linear005: success idris2/linear006: success idris2/linear007: success idris2/linear008: success idris2/linear009: success idris2/linear010: success idris2/linear011: success idris2/linear012: success idris2/literate001: success idris2/literate002: success idris2/literate003: success idris2/literate004: success idris2/literate005: success idris2/literate006: success idris2/literate007: success idris2/literate008: success idris2/literate009: success idris2/literate010: success idris2/literate011: success idris2/literate012: success idris2/literate013: success idris2/literate014: success idris2/literate015: success idris2/literate016: success idris2/namespace001: success idris2/params001: success idris2/perf001: success idris2/perf002: success idris2/perf003: success idris2/perf004: success idris2/perf005: success idris2/perf006: success idris2/perror001: success idris2/perror002: success idris2/perror003: success idris2/perror004: success idris2/perror005: success idris2/perror006: success idris2/pkg001: success idris2/pkg002: success idris2/pkg003: success idris2/pkg004: success idris2/pkg005: success idris2/positivity001: success idris2/positivity002: success idris2/positivity003: success idris2/real001: success idris2/real002: success idris2/record001: success idris2/record002: success idris2/record003: success idris2/record004: success idris2/record005: success idris2/record006: success idris2/reflection001: success idris2/reflection002: success idris2/reflection003: success idris2/reflection004: success idris2/reflection005: success idris2/reflection006: success idris2/reflection007: success idris2/reflection008: success idris2/reflection009: success idris2/reg001: success idris2/reg002: success idris2/reg003: success idris2/reg004: success idris2/reg005: success idris2/reg006: success idris2/reg007: success idris2/reg008: success idris2/reg009: success idris2/reg010: success idris2/reg011: success idris2/reg012: success idris2/reg013: success idris2/reg014: success idris2/reg015: success idris2/reg016: success idris2/reg017: success idris2/reg018: success idris2/reg019: success idris2/reg020: success idris2/reg021: success idris2/reg022: success idris2/reg023: success idris2/reg024: success idris2/reg025: success idris2/reg026: success idris2/reg027: success idris2/reg028: success idris2/reg029: success idris2/reg030: success idris2/reg031: success idris2/reg032: success idris2/reg033: success idris2/reg034: success idris2/reg035: success idris2/total001: success idris2/total002: success idris2/total003: success idris2/total004: success idris2/total005: success idris2/total006: success idris2/total007: success idris2/total008: success idris2/total009: success idris2/total010: success idris2/with001: success idris2/with002: success idris2/with003: success typedd-book/chapter01: success typedd-book/chapter02: success typedd-book/chapter03: success typedd-book/chapter04: success typedd-book/chapter05: success typedd-book/chapter06: success typedd-book/chapter07: success typedd-book/chapter08: success typedd-book/chapter09: success typedd-book/chapter10: success typedd-book/chapter11: success typedd-book/chapter12: success typedd-book/chapter13: success typedd-book/chapter14: success ideMode/ideMode001: success ideMode/ideMode002: success ideMode/ideMode003: success ideMode/ideMode004: success prelude/reg001: success Found Chez at /usr/bin/scheme chez/chez001: FAILURE Expected: [1, 2, 2, 4, 3, 6, 4, 8, 5, 10] 1/1: Building Total (Total.idr) Main> Main> Bye for now! Given: 1/1: Building Total (Total.idr) [1, 2, 2, 4, 3, 6, 4, 8, 5, 10] Main> Main> Bye for now! chez/chez002: FAILURE Expected: [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))] 1/1: Building Pythag (Pythag.idr) Main> Main> Bye for now! Given: 1/1: Building Pythag (Pythag.idr) [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))] Main> Main> Bye for now! chez/chez003: FAILURE Expected: 94 94 188 188 1/1: Building IORef (IORef.idr) Main> Main> Bye for now! Given: 1/1: Building IORef (IORef.idr) 94 94 188 188 Main> Main> Bye for now! chez/chez004: FAILURE Expected: 100 94 94.42 "Hello" "there!" 65535 [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] 00 5E 00 00 00 41 41 41 41 00 7B 14 AE 47 E1 9A .^...AAAA.{..G.. 57 40 00 00 W@.. total size = 20 48 65 6C 6C 6F 20 74 68 65 72 65 21 FF FF 00 00 Hello there!.... 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ total size = 80 1/1: Building Buffer (Buffer.idr) Main> Main> Bye for now! Given: 1/1: Building Buffer (Buffer.idr) 100 94 94.42 "Hello" "there!" 65535 [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] 00 5E 00 00 00 41 41 41 41 00 7B 14 AE 47 E1 9A .^...AAAA.{..G.. 57 40 00 00 W@.. total size = 20 48 65 6C 6C 6F 20 74 68 65 72 65 21 FF FF 00 00 Hello there!.... 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................ total size = 80 Main> Main> Bye for now! chez/chez005: FAILURE Expected: (3 ** [2, 4, 6]) 1/1: Building Filter (Filter.idr) Main> Main> Bye for now! Given: 1/1: Building Filter (Filter.idr) (3 ** [2, 4, 6]) Main> Main> Bye for now! chez/chez006: FAILURE Expected: "Nat" "List of Nat" "List of Something else" "List of Something else" "List of Bool" "Int" "Something else" "List of Type" "List of Int" 43 42 1/1: Building TypeCase (TypeCase.idr) Main> Main> Main.strangeId is total Main> Main.strangeId': strangeId' _ Main> Bye for now! 1/1: Building TypeCase2 (TypeCase2.idr) Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument). TypeCase2.idr:5:14--5:17 | 5 | strangeId {a=Nat} x = x+1 | ^^^ Error: While processing left hand side of foo. Can't match on Nat (Erased argument). TypeCase2.idr:9:5--9:8 | 9 | foo Nat = "Nat" | ^^^ Given: 1/1: Building TypeCase (TypeCase.idr) "Nat" "List of Nat" "List of Something else" "List of Something else" "List of Bool" "Int" "Something else" "List of Type" "List of Int" 43 42 Main> Main> Main.strangeId is total Main> Main.strangeId': strangeId' _ Main> Bye for now! 1/1: Building TypeCase2 (TypeCase2.idr) Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument). TypeCase2.idr:5:14--5:17 | 5 | strangeId {a=Nat} x = x+1 | ^^^ Error: While processing left hand side of foo. Can't match on Nat (Erased argument). TypeCase2.idr:9:5--9:8 | 9 | foo Nat = "Nat" | ^^^ chez/chez007: FAILURE Expected: "Function from Nat to Nat" "Function from Nat to Vector of 0 Int" "Function on Type" 1/1: Building TypeCase (TypeCase.idr) Main> Main> Bye for now! Given: 1/1: Building TypeCase (TypeCase.idr) "Function from Nat to Nat" "Function from Nat to Vector of 0 Int" "Function on Type" Main> Main> Bye for now! chez/chez008: FAILURE Expected: 1 1 1 1/1: Building Nat (Nat.idr) Main> Main> Bye for now! Given: 1/1: Building Nat (Nat.idr) 1 1 1 Main> Main> Bye for now! chez/chez009: FAILURE Expected: 42 ällo 1/1: Building uni (uni.idr) Main> Main> Bye for now! Given: 1/1: Building uni (uni.idr) 42 ällo Main> Main> Bye for now! chez/chez010: FAILURE Expected: 9 Callback coming In callback 24 Callback coming In callback with (1, 2) 3 9 'k' 1/1: Building CB (CB.idr) Main> Main> Bye for now! Given: 1/1: Building CB (CB.idr) 9 Callback coming In callback 24 Callback coming In callback with (1, 2) 3 9 'k' Main> Main> Bye for now! chez/chez011: FAILURE Expected: 5 "12" True False 1/1: Building bangs (bangs.idr) Main> Just 7 Main> Just 7 Main> Main> Main> Main> Main> Bye for now! Given: 1/1: Building bangs (bangs.idr) 5 "12" True False Main> Just 7 Main> Just 7 Main> Main> Main> Main> Main> Bye for now! chez/chez012: FAILURE Expected: [Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing] [Just 1, Just 2, Just 3, Just 4, Just 5] 1/1: Building array (array.idr) Main> Main> Bye for now! Given: 1/1: Building array (array.idr) [Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing] [Just 1, Just 2, Just 3, Just 4, Just 5] Main> Main> Bye for now! chez/chez013: FAILURE Expected: Made it! (40, 30) "Here": (40, 30) 1/1: Building Struct (Struct.idr) Main> Main> Bye for now! Given: 1/1: Building Struct (Struct.idr) Made it! (40, 30) "Here": (40, 30) Main> Main> Bye for now! chez/chez014: FAILURE Expected: Received: hello world! Received: echo: hello world! 1/1: Building Echo (Echo.idr) Main> Main> Bye for now! Given: 1/1: Building Echo (Echo.idr) [server] Failed to bind socket with error: 22 Main> Main> Bye for now! chez/chez015: FAILURE Expected: [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339] [8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357] 1/1: Building Numbers (Numbers.idr) Main> Main> Bye for now! Given: 1/1: Building Numbers (Numbers.idr) [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339] [8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357] Main> Main> Bye for now! chez/chez016: FAILURE Expected: Running Chez program located in folder with spaces 1/1: Building Main (Main.idr) Main> Main> Bye for now! Given: 1/1: Building Main (Main.idr) Running Chez program located in folder with spaces Main> Main> Bye for now! chez/chez017: FAILURE Expected: File Exists False True Just "/home/a/documents/projects/idris2/Idris2-0.3.0/tests/chez/chez017/testdir" 1/1: Building dir (dir.idr) Main> Main> Bye for now! hello Given: 1/1: Building dir (dir.idr) File Exists False True Just "/home/a/documents/projects/idris2/Idris2-0.3.0/tests/chez/chez017/testdir" Main> Main> Bye for now! hello chez/chez018: FAILURE Expected: test test unfinished lineabc def File Not Found 1/1: Building File (File.idr) Main> Main> Bye for now! Given: 1/1: Building File (File.idr) test test unfinished lineabc def File Not Found Main> Main> Bye for now! chez/chez019: FAILURE Expected: ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17 2 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 1/1: Building partial (partial.idr) Main> Main> Main> Main> Main> Bye for now! Given: 1/1: Building partial (partial.idr) ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17 2 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 Main> Main> Main> Main> Main> Bye for now! chez/chez020: FAILURE Expected: opened closed Idris 2 1/1: Building Popen (Popen.idr) Main> Main> Bye for now! Given: 1/1: Building Popen (Popen.idr) opened closed Idris 2 Main> Main> Bye for now! chez/chez021: FAILURE Expected: 1 200 True 200 254 False 248 1 1234567890 255 65535 4294967295 18446744073709551615 1/1: Building Bits (Bits.idr) Main> ["1", "200", "248", "1", "255", "200", "254"] Main> ["True", "False"] Main> ["255", "65535", "4294967295", "18446744073709551615"] Main> Main> Bye for now! Given: 1/1: Building Bits (Bits.idr) 1 200 True 200 254 False 248 1 1234567890 255 65535 4294967295 18446744073709551615 Main> ["1", "200", "248", "1", "255", "200", "254"] Main> ["True", "False"] Main> ["255", "65535", "4294967295", "18446744073709551615"] Main> Main> Bye for now! chez/chez022: FAILURE Expected: Hello Hello Done Free X Freeing 0 Hello Free Y Freeing 1 Hello 1/1: Building usealloc (usealloc.idr) Main> Main> Bye for now! Given: 1/1: Building usealloc (usealloc.idr) Hello Hello Done Free X Freeing 0 Hello Free Y Freeing 1 Hello Main> Main> Bye for now! chez/chez023: FAILURE Expected: Hello 'I' dris! No exceptions occurred 1/1: Building File (File.idr) Main> Main> Bye for now! Given: 1/1: Building File (File.idr) Hello 'I' dris! No exceptions occurred Main> Main> Bye for now! chez/chez024: FAILURE Expected: True HI True HI True EH True Nothing there 1/1: Building Envy (Envy.idr) Main> Main> Bye for now! Given: 1/1: Building Envy (Envy.idr) True HI True HI True EH True Nothing there Main> Main> Bye for now! chez/chez025: FAILURE Expected: 500500 1/1: Building runst (runst.idr) Main> Main> Bye for now! Given: 1/1: Building runst (runst.idr) 500500 Main> Main> Bye for now! chez/chez026: success chez/chez027: FAILURE Expected: hiya 2 Parse failed at position 0: satisfy Parse failed at position 0: Not good ['7', '6', '6', '7', '7', '5'] ['6', '3', '5', '5', '3'] "887" "123" "" True False ['a', '1', 'b', '2'] ['a', 'b', 'c', 'd'] () Parse failed at position 0: Purposefully changed OK to Fail 1/1: Building StringParser (StringParser.idr) Main> Main> Bye for now! Given: 1/1: Building StringParser (StringParser.idr) hiya 2 Parse failed at position 0: satisfy Parse failed at position 0: Not good ['7', '6', '6', '7', '7', '5'] ['6', '3', '5', '5', '3'] "887" "123" "" True False ['a', '1', 'b', '2'] ['a', 'b', 'c', 'd'] () Parse failed at position 0: Purposefully changed OK to Fail Main> Main> Bye for now! chez/chez028: FAILURE Expected: 5678 -3 262145 10 7 1/1: Building ExpressionParser (ExpressionParser.idr) Main> Main> Bye for now! Given: 1/1: Building ExpressionParser (ExpressionParser.idr) 5678 -3 262145 10 7 Main> Main> Bye for now! chez/chez029: FAILURE Expected: ["123", "123", "123", "123", "123"] ["1234", "1234", "1234", "1234"] ["1234567", "1234567", "1234567"] ["134", "134", "134", "134"] ["134", "134", "134", "134"] ["134", "134", "134"] ["134", "134"] ["134"] ["237", "65517", "4294967277", "18446744073709551597"] 1/1: Building BitCasts (BitCasts.idr) Main> Main> Bye for now! Given: 1/1: Building BitCasts (BitCasts.idr) ["123", "123", "123", "123", "123"] ["1234", "1234", "1234", "1234"] ["1234567", "1234567", "1234567"] ["134", "134", "134", "134"] ["134", "134", "134", "134"] ["134", "134", "134"] ["134", "134"] ["134"] ["237", "65517", "4294967277", "18446744073709551597"] Main> Main> Bye for now! chez/chez030: success chez/chez031: success chez/concurrency001: success chez/perf001: success chez/reg001: success Found node at /usr/bin/node node/node001: FAILURE Expected: [1, 2, 2, 4, 3, 6, 4, 8, 5, 10] 1/1: Building Total (Total.idr) Main> Main> Bye for now! Given: 1/1: Building Total (Total.idr) [1, 2, 2, 4, 3, 6, 4, 8, 5, 10] Main> Main> Bye for now! node/node002: FAILURE Expected: [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))] 1/1: Building Pythag (Pythag.idr) Main> Main> Bye for now! Given: 1/1: Building Pythag (Pythag.idr) [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))] Main> Main> Bye for now! node/node003: FAILURE Expected: 94 94 188 188 1/1: Building IORef (IORef.idr) Main> Main> Bye for now! Given: 1/1: Building IORef (IORef.idr) 94 94 188 188 Main> Main> Bye for now! node/node004: FAILURE Expected: 100 94 94.42 "Hello" "there!" 65535 [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] 1/1: Building Buffer (Buffer.idr) Main> Main> Bye for now! Given: 1/1: Building Buffer (Buffer.idr) 100 94 94.42 "Hello" "there!" 65535 [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] [0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] Main> Main> Bye for now! node/node005: FAILURE Expected: (3 ** [2, 4, 6]) 1/1: Building Filter (Filter.idr) Main> Main> Bye for now! Given: 1/1: Building Filter (Filter.idr) (3 ** [2, 4, 6]) Main> Main> Bye for now! node/node006: FAILURE Expected: "Nat" "List of Nat" "List of Something else" "List of Something else" "List of Bool" "Int" "Something else" "List of Type" "List of Int" 43 42 1/1: Building TypeCase (TypeCase.idr) Main> Main> Main.strangeId is total Main> Main.strangeId': strangeId' _ Main> Bye for now! 1/1: Building TypeCase2 (TypeCase2.idr) Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument). TypeCase2.idr:5:14--5:17 | 5 | strangeId {a=Nat} x = x+1 | ^^^ Error: While processing left hand side of foo. Can't match on Nat (Erased argument). TypeCase2.idr:9:5--9:8 | 9 | foo Nat = "Nat" | ^^^ Given: 1/1: Building TypeCase (TypeCase.idr) "Nat" "List of Nat" "List of Something else" "List of Something else" "List of Bool" "Int" "Something else" "List of Type" "List of Int" 43 42 Main> Main> Main.strangeId is total Main> Main.strangeId': strangeId' _ Main> Bye for now! 1/1: Building TypeCase2 (TypeCase2.idr) Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument). TypeCase2.idr:5:14--5:17 | 5 | strangeId {a=Nat} x = x+1 | ^^^ Error: While processing left hand side of foo. Can't match on Nat (Erased argument). TypeCase2.idr:9:5--9:8 | 9 | foo Nat = "Nat" | ^^^ node/node007: FAILURE Expected: "Function from Nat to Nat" "Function from Nat to Vector of 0 Int" "Function on Type" 1/1: Building TypeCase (TypeCase.idr) Main> Main> Bye for now! Given: 1/1: Building TypeCase (TypeCase.idr) "Function from Nat to Nat" "Function from Nat to Vector of 0 Int" "Function on Type" Main> Main> Bye for now! node/node008: FAILURE Expected: 1 1 1 1/1: Building Nat (Nat.idr) Main> Main> Bye for now! Given: 1/1: Building Nat (Nat.idr) 1 1 1 Main> Main> Bye for now! node/node009: FAILURE Expected: 42 ällo 1/1: Building uni (uni.idr) Main> Main> Bye for now! Given: 1/1: Building uni (uni.idr) 42 ällo Main> Main> Bye for now! node/node011: FAILURE Expected: 5 "12" True False 1/1: Building bangs (bangs.idr) Main> Just 7 Main> Just 7 Main> Main> Main> Main> Main> Bye for now! Given: 1/1: Building bangs (bangs.idr) 5 "12" True False Main> Just 7 Main> Just 7 Main> Main> Main> Main> Main> Bye for now! node/node012: FAILURE Expected: [Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing] [Just 1, Just 2, Just 3, Just 4, Just 5] 1/1: Building array (array.idr) Main> Main> Bye for now! Given: 1/1: Building array (array.idr) [Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing] [Just 1, Just 2, Just 3, Just 4, Just 5] Main> Main> Bye for now! node/node015: FAILURE Expected: [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339] [8650625671965379659, 5435549321212129090, 8650625671965378905, 22945956689563340, 102] 1/1: Building Numbers (Numbers.idr) Main> Main> Bye for now! Given: 1/1: Building Numbers (Numbers.idr) [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339] [8650625671965379659, 5435549321212129090, 8650625671965378905, 22945956689563340, 102] Main> Main> Bye for now! node/node017: FAILURE Expected: File Exists False True Just "/home/a/documents/projects/idris2/Idris2-0.3.0/tests/node/node017/testdir" 1/1: Building dir (dir.idr) Main> Main> Bye for now! hello Given: 1/1: Building dir (dir.idr) File Exists False True Just "/home/a/documents/projects/idris2/Idris2-0.3.0/tests/node/node017/testdir" Main> Main> Bye for now! hello node/node018: FAILURE Expected: test test unfinished lineabc def File Not Found 1/1: Building File (File.idr) Main> Main> Bye for now! Given: 1/1: Building File (File.idr) test test unfinished lineabc def File Not Found Main> Main> Bye for now! node/node019: FAILURE Expected: ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17 2 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 1/1: Building partial (partial.idr) Main> Main> Main> Main> Main> Bye for now! Given: 1/1: Building partial (partial.idr) ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17 2 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40 Main> Main> Main> Main> Main> Bye for now! node/node021: FAILURE Expected: 1 200 True 200 254 False 248 1 1234567890 255 65535 4294967295 18446744073709551615 1/1: Building Bits (Bits.idr) Main> ["1", "200", "248", "1", "255", "200", "254"] Main> ["True", "False"] Main> ["255", "65535", "4294967295", "18446744073709551615"] Main> Main> Bye for now! Given: 1/1: Building Bits (Bits.idr) 1 200 True 200 254 False 248 1 1234567890 255 65535 4294967295 18446744073709551615 Main> ["1", "200", "248", "1", "255", "200", "254"] Main> ["True", "False"] Main> ["255", "65535", "4294967295", "18446744073709551615"] Main> Main> Bye for now! node/node022: FAILURE Expected: ["123", "123", "123", "123", "123"] ["1234", "1234", "1234", "1234"] ["1234567", "1234567", "1234567"] ["134", "134", "134", "134"] ["134", "134", "134", "134"] ["134", "134", "134"] ["134", "134"] ["134"] ["237", "65517", "4294967277", "18446744073709551597"] 1/1: Building BitCasts (BitCasts.idr) Main> Main> Bye for now! Given: 1/1: Building BitCasts (BitCasts.idr) ["123", "123", "123", "123", "123"] ["1234", "1234", "1234", "1234"] ["1234567", "1234567", "1234567"] ["134", "134", "134", "134"] ["134", "134", "134", "134"] ["134", "134", "134"] ["134", "134"] ["134"] ["237", "65517", "4294967277", "18446744073709551597"] Main> Main> Bye for now! node/reg001: success node/syntax001: success node/tailrec001: success node/idiom001: success templates/simple-test: success templates/ttimp: success templates/with-ipkg: success 304/349 tests successful make[2]: *** [Makefile:6: test] Error 1 make[2]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0/tests' make[1]: *** [Makefile:86: test] Error 2 make[1]: Leaving directory '/home/a/documents/projects/idris2/Idris2-0.3.0' make: *** [Makefile:172: bootstrap-test] Error 2 ```
nothingnesses commented 3 years ago

Assuming the test outputs are currently buffered, should they instead be ran unbuffered? If it's an issue with stdio redirection in the shell, there's a couple of potential solutions here to that end.

nothingnesses commented 3 years ago

I'm using Bedrock Linux which allows me to use executable binaries built with different libc libraries in the same system. While doing some tests regarding another unrelated issue, I think I've determined that this issue was caused because the Chez Scheme that I was initially using when I posted this issue was built with musl. I tried building and running Idris 2 v0.3.0 again, once using Chez Scheme built with musl and once with one built using glibc. The issue seems to occur only with the Chez Scheme built with musl, but not with the version built with glibc. Would be interested to know if others can replicate this.

FWIW, either version of Chez Scheme seems to be able to run the Idris 2 bootstrapped from the Chez Scheme built with glibc. As I've indicated previously, the musl Chez Scheme causes the tests, and thus the build, to fail, so I can't determine whether the same would be true for an Idris 2 bootstrapped using a musl, instead of glibc, Chez Scheme.

I think #1136 will fix this.

gallais commented 3 years ago

FYI: #1136 has been merged. Let us know if it fixes your issue! :crossed_fingers:

nothingnesses commented 3 years ago

FYI: #1136 has been merged. Let us know if it fixes your issue! crossed_fingers

I've just built and successfully ran the tests for 299a31de5bd64a584a2f7d9090eb2f5680efaeac using Chez Scheme built with musl, so I'm assuming #1136 has indeed fixed the issue. Thanks @nmeum! Closing this.