Cleanup code, bring up to date with new versions of 1Lab and Agda (#21)

RedPRL · Nov 8, 2023 · 0a70440 · 0a70440
1 parent 20fe445
commit 0a70440
Show file tree

Hide file tree

Showing 42 changed files with 1,968 additions and 1,816 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -2,13 +2,13 @@
 # Stage 1: building everything except agda-mugen
 ####################################################################################################
 
-FROM fossa/haskell-static-alpine:ghc-9.0.2 AS agda
+FROM fossa/haskell-static-alpine:ghc-9.4.7 AS agda
 
 WORKDIR /build/agda
 RUN \
   git init && \
   git remote add origin https://github.com/agda/agda.git && \
-  git fetch --depth 1 origin efa6fe4cc65132bcc375f608542154674a37f1ba && \
+  git fetch --depth 1 origin 5c8116227e2d9120267aed43f0e545a65d9c2fe2 && \
   git checkout FETCH_HEAD
 
 # We build Agda and place it in /dist along with its data files.
@@ -36,7 +36,7 @@ WORKDIR /dist/1lab
 RUN \
   git init && \
   git remote add origin https://github.com/plt-amy/1lab && \
-  git fetch --depth 1 origin f5465e947501f971bd2dfb76915e4065b13194c5 && \
+  git fetch --depth 1 origin ac6f81089a261e9c0d2ce3ede37a4a09764cb2ad && \
   git checkout FETCH_HEAD
 RUN echo "/dist/1lab/1lab.agda-lib" > /dist/libraries
 

diff --git a/agda-mugen.agda-lib b/agda-mugen.agda-lib
@@ -1,5 +1,5 @@
 name: agda-mugen
-depend: cubical-1lab
+depend: 1lab
 include:
   src
   wip
@@ -9,4 +9,4 @@ flags:
   --postfix-projections
   --rewriting
   --guardedness
-  -W noNoEquivWhenSplitting
+  -WnoUnsupportedIndexedMatch