Add Idris2 json benchmark

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "json/idris2-json-test"]
+	path = json/idris2-json-test
+	url = https://github.com/Matthew-Mosior/idris2-json-test

README.md

@@ -440,7 +440,7 @@ Base Docker image: Debian GNU/Linux trixie/sid
 | Go               | go1.23.2                        |
 | Go/gccgo         | 14.2.0                          |
 | Haskell          | 9.8.2                           |
-| Idris 2          | 0.6.0                           |
+| Idris 2          | 0.7.0                           |
 | Java             | 23.0.1                          |
 | Julia            | v"1.11.1"                       |
 | Kotlin           | 2.0.21                          |
@@ -555,6 +555,12 @@ TCP connectivity between the tests and the test runner.
  - [raw-strings-qq](http://hackage.haskell.org/package/raw-strings-qq) for
 raw string literals used in tests.
 
+For Idris2:
+ - [elab-util](https://github.com/stefan-hoeck/idris2-elab-util) for idris2-json-test.
+ - [parser-json](https://github.com/stefan-hoeck/idris2-parser/tree/main/json) for idris2-json-test.
+ - [ref1](https://github.com/stefan-hoeck/idris2-ref1) for idris2-json-test.
+ - [network](https://test.idris-lang.org/Idris2/network/) for TCP connectivity between the tests and the test runner.
+
 For Perl:
 
  - [cpanminus](https://metacpan.org/pod/App::cpanminus) for installing

brainfuck/Makefile

@@ -28,8 +28,7 @@ executables := \
 	target/bin_c_clang \
 	fsharp/target/Release/net8.0/brainfuck \
 	target/Release/net8.0/brainfuck \
-	target/bin_zig \
-	target/bin_idris
+	target/bin_zig
 
 artifacts := $(executables) \
 	target/bf2-kt.jar \
@@ -151,16 +150,14 @@ target/bf.class: bf.java | target
 target/bin_zig: bf.zig | $(zig_fmt)
 	$(ZIG_BUILD)
 
-target/bin_idris: bf.idr | target
-	$(IDRIS_BUILD)
-
 # Run
 
 .PHONY: run
 run: $(all_runners)
 
 .PHONY: run2
 run2: BF_SRC := mandel.b > /dev/null
+
 run2: $(fast_runners)
 
 ## Common recipe for all runners

brainfuck/bf-marray.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE PackageImports #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
@@ -17,7 +18,7 @@ import Network.Socket.ByteString
 import System.Environment
 import System.Exit
 import System.IO (hFlush, stdout)
-import System.Posix (getProcessID)
+import "unix" System.Posix (getProcessID)
 import Text.RawString.QQ
 
 data Op = Inc !Int | Move !Int | Print | Loop ![Op] deriving Show

brainfuck/bf.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE PackageImports #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
@@ -15,7 +16,7 @@ import Network.Socket.ByteString
 import System.Environment
 import System.Exit
 import System.IO
-import System.Posix (getProcessID)
+import "unix" System.Posix (getProcessID)
 
 data Op = Inc !Int | MoveLeft | MoveRight | Print | Loop [Op]
 data Tape = Tape { left :: [Int], current :: !Int, right :: [Int] }

brainfuck/bf.idr

@@ -49,19 +49,16 @@ accCheckSum : Int -> (Int, Int) -> (Int, Int)
 accCheckSum n (s₁, s₂) = let s₁' = (s₁ + n) `mod` 255
                              s₂' = (s₁' + s₂) `mod` 255
                          in (s₁', s₂')
-
 -- For benchmark
 Loud = IO
 Ctx Loud where
   write n = do
     putChar (chr n)
     fflush stdout
-
 -- For checksum-ing
 Quiet = State (Int, Int)
 Ctx Quiet where
   write n = modify (accCheckSum n)
-
 partial
 run : Ctx m => List Op -> Tape -> m Tape
 run [] tape = pure tape

common/commands.mk

@@ -53,32 +53,34 @@ endef
 
 ECHO_RUN = @tput bold; echo "$(MAKE) $@"; tput sgr0
 XTIME := ../xtime.rb
+XTIME_IDRIS := ../../xtime.rb
 CPANM := cpanm -l ~/perl5
 
-CLOJURE_RUN =		$(XTIME) clojure $(CLOJURE_FLAGS) -M $^
-ELIXIR_RUN =		$(XTIME) elixir $^
-EXECUTABLE_RUN =	$(XTIME) $^
-JAVA_CLASS_RUN =	$(XTIME) java -cp $(^D) $(basename $(^F))
-JAVA_JAR_RUN =		$(XTIME) java -jar $^
-JRUBY_RUN =		$(XTIME) jruby $^
-LUA_JIT_RUN =		$(XTIME) luajit $^
-LUA_RUN =		$(XTIME) lua $^
-MONO_RUN =		$(XTIME) mono -O=all --gc=sgen $^
-NODE_RUN =		$(XTIME) node $^
-PERL_RUN =		$(XTIME) perl -I ~/perl5/lib/perl5 $^
-PHP_RUN =		$(XTIME) php $^
-PYPY3_RUN =		$(XTIME) pypy3 $^
-PYTHON3_RUN =		$(XTIME) python3 $^
-RACKET_RUN =		PLT_CS_COMPILE_LIMIT=100000 $(XTIME) racket $^
-RUBY_JIT_RUN =		$(XTIME) ruby --jit $^
-RUBY_RUN =		$(XTIME) ruby $^
-SCALA_RUN =		$(XTIME) scala $^
-TCLSH_RUN =		$(XTIME) tclsh $^
-TRUBY_JVM_RUN =		$(XTIME) truffleruby-jvm-bin $^
-TRUBY_NATIVE_RUN =	$(XTIME) truffleruby $^
-SCHEME_RUN =		$(XTIME) scheme --optimize-level 3 --program $^
-JULIA_RUN =		$(XTIME) julia --optimize=3 --check-bounds=no $^
-PHP_RUN =		$(XTIME) php $^
+CLOJURE_RUN =			$(XTIME) clojure $(CLOJURE_FLAGS) -M $^
+ELIXIR_RUN =			$(XTIME) elixir $^
+EXECUTABLE_RUN =		$(XTIME) $^
+JAVA_CLASS_RUN =		$(XTIME) java -cp $(^D) $(basename $(^F))
+JAVA_JAR_RUN =			$(XTIME) java -jar $^
+JRUBY_RUN =			$(XTIME) jruby $^
+LUA_JIT_RUN =			$(XTIME) luajit $^
+LUA_RUN =			$(XTIME) lua $^
+MONO_RUN =			$(XTIME) mono -O=all --gc=sgen $^
+NODE_RUN =			$(XTIME) node $^
+PERL_RUN =			$(XTIME) perl -I ~/perl5/lib/perl5 $^
+PHP_RUN =			$(XTIME) php $^
+PYPY3_RUN =			$(XTIME) pypy3 $^
+PYTHON3_RUN =			$(XTIME) python3 $^
+RACKET_RUN =			PLT_CS_COMPILE_LIMIT=100000 $(XTIME) racket $^
+RUBY_JIT_RUN =			$(XTIME) ruby --jit $^
+RUBY_RUN =			$(XTIME) ruby $^
+SCALA_RUN =			$(XTIME) scala $^
+TCLSH_RUN =			$(XTIME) tclsh $^
+TRUBY_JVM_RUN =			$(XTIME) truffleruby-jvm-bin $^
+TRUBY_NATIVE_RUN =		$(XTIME) truffleruby $^
+SCHEME_RUN =			$(XTIME) scheme --optimize-level 3 --program $^
+JULIA_RUN =			$(XTIME) julia --optimize=3 --check-bounds=no $^
+PHP_RUN =			$(XTIME) php $^
+IDRIS_JSON_BUILD_AND_RUN =      cd idris2-json-test && pack build && $(XTIME_IDRIS) pack run idris2-json-test.ipkg
 
 GIT_CLONE = git clone --depth 1 -q
 DOTNET_CLEAN = -dotnet clean --nologo -v q -c Release

docker/Dockerfile

@@ -1,4 +1,5 @@
-FROM debian:trixie-20241016-slim
+FROM debian:trixie-20240701-slim
+
 
 ENV APT_KEY_DONT_WARN_ON_DANGEROUS_USAGE=1 \
     DEBIAN_FRONTEND=noninteractive
@@ -10,7 +11,6 @@ RUN apt-get update && apt-get install -y --no-install-recommends \
 
 RUN apt-get update && apt-get install -y --no-install-recommends \
     build-essential \
-    chezscheme \
     clang-19 \
     cmake \
     cpanminus \
@@ -21,7 +21,6 @@ RUN apt-get update && apt-get install -y --no-install-recommends \
     gdc-14 \
     git \
     libblas-dev \
-    libboost-dev \
     libc++-19-dev \
     libc++abi-19-dev \
     libevent-dev \
@@ -44,6 +43,7 @@ RUN apt-get update && apt-get install -y --no-install-recommends \
     libssl-dev \
     libtool \
     libtool-bin \
+    libx11-dev \
     libxml2 \
     libyajl-dev \
     libyaml-dev \
@@ -88,16 +88,22 @@ ENV PATH="/root/bin/:/root/.local/bin/:${PATH}" \
 RUN curl -Lo /root/bin/coursier https://git.io/coursier-cli \
     && chmod +x /root/bin/coursier
 
-# https://www.idris-lang.org/pages/download.html
-ARG IDRIS=0.6.0
-RUN curl https://www.idris-lang.org/idris2-src/idris2-$IDRIS.tgz | tar -xz
-WORKDIR /root/bin/Idris2-$IDRIS
-ENV PATH="/root/bin/idris2/bin:${PATH}"
-ENV LD_LIBRARY_PATH="/root/bin/idris2/lib"
-RUN PREFIX=/root/bin/idris2 make bootstrap SCHEME=chezscheme \
-    && PREFIX=/root/bin/idris2 make install
+# https://github.com/cisco/ChezScheme
+WORKDIR /root/bin
+RUN git clone https://github.com/cisco/ChezScheme.git
+WORKDIR /root/bin/ChezScheme
+RUN ./configure
+RUN make
+RUN make install
+
+# https://github.com/stefan-hoeck/idris2-pack
+ENV PACK_DIR="/root/bin/.pack"
 WORKDIR /root/bin
-RUN rm -rf Idris2-$IDRIS
+RUN echo -e "scheme" | bash -c "$(curl -fsSL https://raw.githubusercontent.com/stefan-hoeck/idris2-pack/main/install.bash)"
+ENV PATH="${PACK_DIR}/bin:${PACK_DIR}/.idris2/bin:${PATH}"
+RUN pack install elab-util
+RUN pack install parser-json
+RUN pack install ref1
 
 # https://www.ruby-lang.org/en/downloads/
 ARG RUBY=ruby-3.3.5
@@ -247,15 +253,16 @@ ENV PATH="/root/bin/opam/ocaml-base-compiler.$OCAML/bin/:${PATH}"
 
 # https://kotlinlang.org/docs/command-line.html
 ARG KOTLIN=2.0.21
-RUN curl -LO \
+RUN curl -L -o kotlin-compiler-$KOTLIN.zip \
     https://github.com/JetBrains/kotlin/releases/download/v$KOTLIN/kotlin-compiler-$KOTLIN.zip \
     && unzip kotlin-compiler-$KOTLIN.zip \
     && rm kotlin-compiler-$KOTLIN.zip
 ENV PATH="/root/bin/kotlinc/bin/:${PATH}"
 
 # https://download.racket-lang.org/
 ARG RACKET=8.14
-RUN curl -LO \
+RUN curl -L -o racket-$RACKET-x86_64-linux-cs.sh \
+
     https://download.racket-lang.org/installers/$RACKET/racket-$RACKET-x86_64-linux-cs.sh \
     && sh racket-$RACKET-x86_64-linux-cs.sh --unix-style --dest /root/ \
     && rm racket-$RACKET-x86_64-linux-cs.sh
@@ -280,7 +287,7 @@ ENV PATH="/root/bin/luajit/bin:${PATH}"
 
 # https://github.com/vlang/v/releases
 ARG VLANG=0.4.8
-RUN curl -LO \
+RUN curl -Lo v_linux.zip \
     https://github.com/vlang/v/releases/download/$VLANG/v_linux.zip \
     && unzip -q v_linux.zip \
     && rm v_linux.zip
@@ -312,10 +319,14 @@ RUN ghcup install ghc $GHC_VER && ghcup set ghc $GHC_VER
 
 # Shared packages for all Haskell code
 RUN cabal update \
-    && cabal install network raw-strings-qq unix bytestring array --lib \
+    && cabal install bytestring-0.12.1.0 network-3.2.7.0 raw-strings-qq unix-2.8.6.0 array --lib \
     && cabal install hlint
 ENV GHC_PACKAGE_PATH="~/.cabal/store/ghc-${GHC_VER}/package.db:"
 
+# Hide unnecessary package (Haskell).
+#RUN ghc-pkg hide bytestring-0.12.1.0
+#RUN ghc-pkg hide unix-2.8.4.0 
+
 ARG SCRIPTS_VER=unknown
 COPY *.rb ./
 

json/Makefile

@@ -75,6 +75,7 @@ artifacts := $(executables) \
 
 #	run[test.jl] 
 all_runners := $(patsubst %,run[%], $(artifacts)) \
+	run[idris2-json-test] \
 	run[test_yajl.rb] \
 	run[test.pl] \
 	run[test-xs.pl] \
@@ -411,6 +412,9 @@ run[test.clj]:: run[%]: %
 run[test.rkt]:: run[%]: %
 	$(RACKET_RUN)
 
+run[idris2-json-test]:: run[%]: %
+	$(IDRIS_JSON_BUILD_AND_RUN)
+
 # Utilities
 
 .PHONY: clean