Merge pull request #167 from input-output-hk/bwbush/pc2

Implemented `chainWeight` in Agda and reorganized packages and build
input-output-hk · Jul 3, 2024 · 520eba1 · 520eba1
2 parents bd2e07e + 88b7379
commit 520eba1
Show file tree

Hide file tree

Showing 28 changed files with 120 additions and 320 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -77,9 +77,6 @@ jobs:
           trusted-public-keys = ${{ env.TRUSTED_PUBLIC_KEYS }}
           substituters = ${{ env.SUBSTITUTERS }}
           experimental-features = nix-command flakes
-    - name: 🔬 Test with `peras-hs-test`
-      run: |
-        nix run .#peras-hs-test
     - name: 🔬 Test with `peras-simulation-test`
       run: |
         nix run .#peras-simulation-test

diff --git a/Makefile b/Makefile
@@ -2,7 +2,7 @@
 AGDAFILES := $(shell find src -name *.agda -exec grep -l AGDA2HS {} \;)
 LAGDAFILES := $(shell find src -name *.lagda.md -exec grep -l AGDA2HS {} \;)
 SIMAGDAFILES := $(shell find sim_src -name *.agda -exec grep -l AGDA2HS {} \;)
-HSDIR=peras-hs
+HSDIR=peras-simulation
 HSFILES := $(patsubst %.agda,$(HSDIR)/%.hs,$(AGDAFILES))
 LHSFILES := $(patsubst %.lagda.md,$(HSDIR)/%.hs,$(LAGDAFILES))
 SIMHSFILES := $(patsubst sim_src/%.agda,peras-simulation/src/%.hs,$(SIMAGDAFILES))
@@ -18,29 +18,22 @@ $(info $(LHSFILES))
 .PHONY: typecheck
 
 all: typecheck
-	cabal update
 	cabal build all
 
 typecheck: $(HSFILES) $(LHSFILES) $(SIMHSFILES)
-	@rm -f $(BADSIMHSFILES)
 
-# From https://stackoverflow.com/questions/34621364/makefile-compile-o-from-c-files
 $(HSDIR)/%.hs: %.agda
+	@$(AGDA) --local-interfaces --library-file=$(AGDA_LIBS) $^
 	@$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src --config $(AGDA2HS_CONFIG) $^
-	@$(AGDA) --compile --ghc-dont-call-ghc --no-main --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^
 
 $(HSDIR)/%.hs: %.lagda.md
+	@$(AGDA) --local-interfaces --library-file=$(AGDA_LIBS) $^
 	@$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src --config $(AGDA2HS_CONFIG) $^
-	@$(AGDA) --compile --ghc-dont-call-ghc --no-main --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=$(HSDIR)/src $^
 
-peras-simulation/src/%.hs : sim_src/%.agda
-	@$(AGDA2HS) --local-interfaces --library-file=$(AGDA_LIBS) --compile-dir=peras-simulation/src $^
+.PHONY : clean
 
-.PHONY : clean veryclean
 clean:
 	@echo "Removing .agdai files"
 	@find src -name \*.agdai -delete;
-
-veryclean: clean
-	@echo "Removing generated.hs files"
-	@rm $(HSFILES) $(LHSFILES)
+	@echo "Removing generated .hs files"
+	@rm -f $(HSFILES) $(LHSFILES)
diff --git a/cabal.project b/cabal.project
@@ -15,7 +15,6 @@ index-state:
   , cardano-haskell-packages 2024-05-29T10:15:00Z
 
 packages:
-  peras-hs
   peras-simulation
   peras-markov
   peras-server

diff --git a/nix/agda-project.nix b/nix/agda-project.nix
@@ -3,7 +3,7 @@
 pkgs.haskell-nix.hackage-project {
   name = "Agda";
 
-  version = "2.6.4.1";
+  version = "2.6.4.3";
 
   compiler-nix-name = "ghc96";
 

diff --git a/peras-hs/LICENSE b/peras-hs/LICENSE
diff --git a/peras-hs/ReadMe.md b/peras-hs/ReadMe.md
diff --git a/peras-hs/peras-hs.cabal b/peras-hs/peras-hs.cabal
diff --git a/peras-hs/test/Main.hs b/peras-hs/test/Main.hs
diff --git a/peras-hs/golden/Event.json → peras-simulation/golden/Event.json b/peras-hs/golden/Event.json → peras-simulation/golden/Event.json
diff --git a/peras-hs/golden/[Block].json → peras-simulation/golden/[Block].json b/peras-hs/golden/[Block].json → peras-simulation/golden/[Block].json