From 9673ba55516cab99ebba4dba41f9428c06347947 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 9 Sep 2024 17:51:46 -0400
Subject: [PATCH 1/2] update build process

---
 Makefile          | 15 ++++++++++++++-
 driver/Main.ml    |  2 +-
 driver/Mcltt.ml   | 11 +++++++++++
 driver/dune       |  5 +++++
 theories/Makefile | 18 +++++++++++++++++-
 5 files changed, 48 insertions(+), 3 deletions(-)
 create mode 100644 driver/Mcltt.ml

diff --git a/Makefile b/Makefile
index 07ab78cc..9be693c3 100644
--- a/Makefile
+++ b/Makefile
@@ -1 +1,14 @@
-# TODO: redo this makefile properly
+EXECUTABLE:=_build/default/driver/mcltt.exe
+
+.PHONY: all clean
+
+all:
+	@cd theories; make
+	@dune build
+
+clean:
+	@cd theories; make clean
+	@dune clean
+	@echo "Cleaning finished."
+
+${EXECUTABLE}: all
diff --git a/driver/Main.ml b/driver/Main.ml
index 435a30c2..5b847973 100644
--- a/driver/Main.ml
+++ b/driver/Main.ml
@@ -24,6 +24,6 @@ let main ?(default_fp = "") () =
         with
         | Failure s -> prerr_string s; raise Exit) in
   let token_stream = loop (Lexing.from_channel chan) in
-  let res = Entrypoint.main max_int token_stream in
+  let res = Entrypoint.main 500 token_stream in
   Format.printf "%a@."
     PrettyPrinter.format_main_result res
diff --git a/driver/Mcltt.ml b/driver/Mcltt.ml
new file mode 100644
index 00000000..8a26400d
--- /dev/null
+++ b/driver/Mcltt.ml
@@ -0,0 +1,11 @@
+open Mcltt.Main
+
+let () =
+  if Array.length Sys.argv <> 2 then
+    begin
+      Printf.fprintf stderr "incorrect input: %s <input-file>\n" Sys.argv.(0);
+      exit 1
+    end;
+  let filename = Sys.argv.(1) in
+  main ~default_fp:filename ();
+  exit 0
diff --git a/driver/dune b/driver/dune
index d0049195..4b347eb0 100644
--- a/driver/dune
+++ b/driver/dune
@@ -9,6 +9,11 @@
  ;  (pps ppx_inline_test))
 )
 
+(executable
+ (name mcltt)
+ (modules Mcltt)
+ (libraries Mcltt))
+
 (env
  (dev
   (flags
diff --git a/theories/Makefile b/theories/Makefile
index cb16c21e..e34b6489 100644
--- a/theories/Makefile
+++ b/theories/Makefile
@@ -1,3 +1,19 @@
+NPROCS := 1
+OS := $(shell uname)
+export NPROCS
+
+ifeq ($J,)
+
+ifeq ($(OS),Linux)
+  NPROCS := $(shell grep -c ^processor /proc/cpuinfo)
+else ifeq ($(OS),Darwin)
+  NPROCS := $(shell system_profiler | awk '/Number of CPUs/ {print $$4}{next;}')
+endif # $(OS)
+
+else
+  NPROCS := $J
+endif # $J
+
 empty :=
 space := $(empty) $(empty)
 
@@ -19,7 +35,7 @@ COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
 
 .PHONY: all
 all: $(COQMAKEFILE)
-	@+$(MAKE) -f "$(COQMAKEFILE)" all
+	@+$(MAKE) -j "${NPROCS}" -f "$(COQMAKEFILE)" all
 
 .PHONY: clean
 clean: $(COQMAKEFILE)

From 025445119c06ae3e697229bec7f96c9cfdd6c392 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Mon, 9 Sep 2024 18:08:37 -0400
Subject: [PATCH 2/2] address issues and update CI

---
 .github/workflows/ci_build.yaml | 6 +++---
 Makefile                        | 8 ++------
 driver/Mcltt.ml                 | 3 +--
 3 files changed, 6 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/ci_build.yaml b/.github/workflows/ci_build.yaml
index c0655c87..bfa86005 100644
--- a/.github/workflows/ci_build.yaml
+++ b/.github/workflows/ci_build.yaml
@@ -61,9 +61,9 @@ jobs:
               make -j ${{ steps.cpu-cores.outputs.count }} pretty-timed
             endGroup
           after_script: |
-            startGroup "Test parser"
-              dune build
-              dune runtest
+            startGroup "Build binary"
+              cd ..
+              make
             endGroup
           export: "OPAMJOBS OPAMYES"
         env:
diff --git a/Makefile b/Makefile
index 9be693c3..2f1df769 100644
--- a/Makefile
+++ b/Makefile
@@ -1,14 +1,10 @@
-EXECUTABLE:=_build/default/driver/mcltt.exe
-
 .PHONY: all clean
 
 all:
-	@cd theories; make
+	@make -C theories
 	@dune build
 
 clean:
-	@cd theories; make clean
+	@make clean -C theories
 	@dune clean
 	@echo "Cleaning finished."
-
-${EXECUTABLE}: all
diff --git a/driver/Mcltt.ml b/driver/Mcltt.ml
index 8a26400d..816004bf 100644
--- a/driver/Mcltt.ml
+++ b/driver/Mcltt.ml
@@ -7,5 +7,4 @@ let () =
       exit 1
     end;
   let filename = Sys.argv.(1) in
-  main ~default_fp:filename ();
-  exit 0
+  main ~default_fp:filename ()