update build process

.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:

Makefile

@@ -1 +1,10 @@
-# TODO: redo this makefile properly
+.PHONY: all clean
+
+all:
+	@make -C theories
+	@dune build
+
+clean:
+	@make clean -C theories
+	@dune clean
+	@echo "Cleaning finished."

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

driver/Mcltt.ml

@@ -0,0 +1,10 @@
+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 ()

driver/dune

@@ -9,6 +9,11 @@
  ;  (pps ppx_inline_test))
 )
 
+(executable
+ (name mcltt)
+ (modules Mcltt)
+ (libraries Mcltt))
+
 (env
  (dev
   (flags

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)