Working release

.github/copilot-instructions.md

@@ -0,0 +1,65 @@
+# Copilot Instructions for stelf
+
+## Quick build / test / lint commands
+- dune build                # build (many modules may fail; expected)
+- dune build @check         # fast type-check only
+- dune runtest              # run all tests
+- dune exec bin/main.exe    # run Pal frontend (REPL/CLI)
+- dune fmt                  # format (ocamlformat 0.28.1)
+- make build/test/docs      # Makefile targets: `make build`, `make test`, `make docs`
+- make check                # runs `dune build @check` via Makefile
+
+Running a single test
+- Two Alcotest suites live under test/:
+  - test/Pal/PalTest.ml  → dune exec test/Pal/PalTest.exe
+  - test/Parse/ParseTest.ml → dune exec test/Parse/ParseTest.exe -- test '<suite>' <n>
+- For debugging a failing test: run its executable directly (dune exec ...), read output, then inspect the test file in test/*/Cases.ml.
+
+Notes
+- Do NOT use `dune utop` or `make repl` — utop preloads compiler-libs which conflicts with project modules (e.g., Lambda, Lexer, Parser).
+- The `basis/` directory is a pinned submodule providing SML basis shims. Clone with submodules:
+  git clone --recurse-submodules <repo>
+  or: git submodule update --init
+
+## High-level architecture (big picture)
+- ~40 Dune libraries under src/, layered roughly:
+  - Foundation: global, trail, table, stream, timing
+  - Core LF: src/IntSyn (IntSyn, Whnf, Conv, Unify, Abstract)
+  - Middle: names, paths, print, index, modes, subordinate, typecheck, modules
+  - Analysis: terminate, thm, cover, meta, prover, tomega
+  - Execution: compile, opsem, solvers
+  - Frontend: src/frontend (Lexer, Parser, Recon*, Twelf_, Frontend_, Solve)
+- Two frontend variants to know: `modern` (parser) and `pal` (combined frontend used by bin/main.exe).
+- Many modules are wired by functor instantiation in *_.sml.ml files; top-level wiring is in src/frontend/frontend_.sml.ml.
+
+## Key repository conventions (non-obvious)
+- Two source styles:
+  - Old-style (most src/*): three-part module pattern concatenated by Dune:
+    - .sig.ml (signature), .fun.ml (functor implementation), .sml.ml (instantiation/wiring)
+    - Check `sources.dune` files in subdirs for concatenation rules.
+  - New-style (src/Common, src/Recon, src/Lang, src/frontend, src/Fronts): single-file modules and explicit interfaces.
+- Naming:
+  - SML structure → OCaml `module Foo`
+  - SML signature → `module type FOO`
+  - Functors → `module MakeFoo(...)` or `module Foo(...)`
+  - Constructors colliding with OCaml keywords append `_` (ok_, abort_, Type_)
+- Compatibility:
+  - Old-style files `open Basis` and prefer Basis.* (Basis.Array, Basis.List) over OCaml stdlib.
+  - Old-style libraries: `wrapped = false` and build flags include `-w -A -open Basis`.
+  - New code should be `wrapped = true`.
+- Formatting: ocamlformat 0.28.1 (default profile).
+- Tests: test cases are in test/*/Cases.ml; Common.ml has helpers.
+- Submodules: `basis/` and `twelf/` are submodules; ensure initialized when building.
+
+## Where to look first when investigating
+1. Re-run the failing test (dune exec path/to/Exe) and read its output.
+2. Open the test Cases.ml and the code under test in src/ that the test imports.
+3. Limit early file reads to ~3 files; then form a hypothesis before deeper searches.
+4. Use `dune build @check` to perform a fast type-check.
+
+## Other AI/assistant configs in repo
+- CLAUDE.md (project guidance for Claude)
+- .github/agents/ocaml-doc-converter.agent.md
+- Keep these in sync when updating instructions.
+
+Summary: updated instructions include exact Makefile/dune commands, single-test examples, submodule notes, and the three-file module convention.

.gitmodules

@@ -5,3 +5,6 @@
 [submodule "twelf"]
 	path = twelf
 	url = https://github.com/standardml/twelf
+[submodule "stelf-book"]
+	path = stelf-book
+	url = https://github.com/standardocaml/stelf-book.git

.ocamlformat

@@ -1,2 +1 @@
-
-profile=default
+profile=default

Makefile

@@ -1,31 +1,64 @@
-BUILD_DIR ?= _build/default
-DUNE ?= dune
+TARGET         ?= ./stelf
+DUNE_LOCK      ?= ./dune.lock/
+OPAM_FILE      ?= ./stelf.opam
+DUNE_BUILD_DIR ?= _build/default
+DUNE_MIN_VERSION ?= 3.23
+DUNE_PROJECT   ?= ./dune-project
+SWITCH         ?= .
+OPAM           ?= opam
+OPAM_EXEC      := $(OPAM) exec --switch $(SWITCH) --
+DUNE           ?= dune
 
-.PHONY: all build test docs install clean repl check help
+SWITCH_SENTINEL := _opam/.opam-switch/switch-config
+DUNE_SENTINEL   := _opam/lib/dune/META
+DEPS_SENTINEL   := .deps-installed
 
-all: build test docs install 
+.PHONY: all build test install docs clean check lock
 
+all: build
 
-build:
-	@$(DUNE) build
+# Phase 1: initialize opam if needed, then create the local switch
+$(SWITCH_SENTINEL):
+	$(OPAM) init --bare --no-setup --yes 2>/dev/null || true
+	$(OPAM) switch create $(SWITCH) --empty --yes 2>/dev/null || true
+	@test -f $@ || (echo "ERROR: opam switch creation failed"; exit 1)
 
+# Phase 2: install OCaml compiler + dune >= $(DUNE_MIN_VERSION) into the switch
+$(DUNE_SENTINEL): $(SWITCH_SENTINEL)
+	$(OPAM) install --switch $(SWITCH) --yes \
+	    "ocaml>=5.0.0" "dune>=$(DUNE_MIN_VERSION)"
 
-check: 
-	@$(DUNE) build @check
+# Phase 3: ensure submodules are present, then generate stelf.opam from dune-project
+# dune.lock/ is committed — re-locking is done explicitly via `make lock`
+$(OPAM_FILE): $(DUNE_PROJECT) $(DUNE_SENTINEL)
+	git submodule update --init --recursive
+	$(OPAM_EXEC) $(DUNE) build $(OPAM_FILE)
 
-repl:
-	@$(DUNE) utop
+# Phase 4: install all package dependencies into the local switch
+$(DEPS_SENTINEL): $(OPAM_FILE)
+	$(OPAM) install --switch $(SWITCH) . --deps-only --yes
+	@touch $@
 
-test:
-	@$(DUNE) runtest
+build: $(DEPS_SENTINEL)
+	$(OPAM_EXEC) $(DUNE) build
+	cp $(DUNE_BUILD_DIR)/bin/main.exe $(TARGET)
 
-docs:
-	@$(DUNE) build @doc
+test: $(DEPS_SENTINEL)
+	$(OPAM_EXEC) $(DUNE) runtest
 
-install:
-	@$(DUNE) install
+check: $(DEPS_SENTINEL)
+	$(OPAM_EXEC) $(DUNE) build @check
 
+install: build
+	$(OPAM_EXEC) $(DUNE) install --prefix _opam
 
-clean:
-	@$(DUNE) clean
+docs: $(DEPS_SENTINEL)
+	$(OPAM_EXEC) $(DUNE) build @doc
+
+# Explicitly refresh the lock file (requires network; updates dune.lock/)
+lock: $(DUNE_SENTINEL)
+	$(OPAM_EXEC) $(DUNE) pkg lock
 
+clean:
+	$(OPAM_EXEC) $(DUNE) clean
+	rm -f $(TARGET) $(DEPS_SENTINEL)

README.md

@@ -2,6 +2,10 @@
 
 This is the STELF project, a port of the Twelf system to OCaml, and subsequents developments thereof.
 
+> [!warning] If you get `dune` seeming to be "paused" on building, or the number of tasks increasing, your computer (probably) won't explode. 
+> This is merely an artificat of the new Dune package managment system (the first pause is due to the ocaml compiler).
+> If you want to make sure nothing is going wrong, add `--verbose` to the `dune build` command, and you should see the tasks being built one by one.
+
 ## Twelf Port 
 
 The Twelf port, which is completed, involved translating between SML to OCaml, and also the creation of a temporary basis library.

STYLE.md

@@ -0,0 +1,22 @@
+# Style Guide 
+
+> [!NOTE] This list is not exhaustive. Also, a number of these are not yet correctly used.
+
+Avoid names ending in underscores, esspecially if they don't conflict with another name.
+Use `snake_case` for lowercase names, and `CamelCase` for uppercase names. The only exception to this is that `Make_` should be used as a prefix for functors, as `Make_HashMap`
+
+A module `Foo` should be of module type `FOO`.
+Each library should have a top level interface, `*.mli`.
+
+If there is a module `Foo`, then it should be defined in `Foo.ml`, and its interface should be defined in `FOO.ml`, prefer `Foo.ml` to `foo.ml`, and `FOO.ml` to `Foo_intf.ml` or `foo_intf.ml`.
+
+In this case, the module should look like this 
+
+```ocaml
+module type FOO = FOO.FOO
+module Foo : FOO = struct 
+  (* Implementation here *)
+end
+```
+
+All module types should be documented 

bin/dune

@@ -2,4 +2,4 @@
  (name main)
  (public_name stelf)
  (modules main)
- (libraries stelf server pal))
+ (libraries stelf server pal cmdliner fmt.tty display basis lwt.unix grace grace.ansi_renderer))

bin/main.ml

@@ -1,12 +1,89 @@
-(*
-(** Entry point for the STELF server executable. *)
+module P = Pal
 
-module Twelf_server = Server.Server_.Server
-
-(** Run the server process and return its exit code. *)
-let run_server () : int = Twelf_server.server ("stelf", [])
-
-let () = if run_server () = 0 then exit 0 else exit 1
-*)
-
-let () = Pal.Pal.run ()
+let () =
+  let open P.Pal in
+  let open Cmdliner in
+  let open Cmdliner.Term.Syntax in
+  let version = P.version in
+  let repl_cmd : int Cmd.t =
+    let config_file =
+      Arg.(value & pos 0 (some file) None & info [] ~docv:"CONFIG"
+             ~doc:"Optional .toml project file to load before entering the REPL")
+    in
+    let repl_fn : int Term.t =
+      let+ verbosity = Arg.value P.Opts.Opts.verbosity
+      and+ color = Arg.value P.Opts.Opts.color
+      and+ unicode = Arg.value P.Opts.Opts.unicode
+      and+ config = config_file in
+      let module N = struct
+        let use_color = color
+        let use_unicode = unicode
+        let verbosity = verbosity
+      end in
+      Lwt_main.run (top ?config:(Option.map Fpath.v config) (module N))
+    and repl_info : Cmd.info =
+      Cmd.info "repl" ~doc:"Start the interactive REPL, optionally loading a project config"
+    in
+    Cmd.v repl_info repl_fn
+  in
+  let check_cmd : int Cmd.t =
+    let file =
+      Arg.(required & pos 0 (some file) None & info [] ~docv:"FILE")
+    in
+    Cmd.v
+      (Cmd.info "check" ~doc:"Load a .cfg or source file")
+      Term.(
+        const (fun verbosity f ->
+            Fmt_tty.setup_std_outputs ();
+            M.chatter := Display.Info.to_int verbosity;
+            Display.register (fun m ->
+                if Display.Info.(m.level =< verbosity) then begin
+                  let open Grace.Diagnostic.Severity in
+                  let pp_diag fmt d = Grace_ansi_renderer.pp_diagnostic fmt d in
+                  let display_diag sev =
+                    let diag =
+                      Grace.Diagnostic.create sev
+                        (fun ppf -> Display.fmt ppf m.msg)
+                    in
+                    Format.printf "%a%!" pp_diag diag
+                  in
+                  match m.kind with
+                  | Some Display.Error -> display_diag Error
+                  | Some Display.Warning -> display_diag Warning
+                  | Some Display.Response ->
+                    Format.printf "=> %t\n%!" m.msg
+                  | _ -> display_diag Note
+                end;
+                Lwt.return ());
+            status_to_exit @@ M.make (File (Fpath.v f)))
+        $ Arg.value P.Opts.Opts.verbosity
+        $ file)
+  in
+  let version_cmd : int Cmd.t =
+    Cmd.v
+      (Cmd.info "version" ~doc:"Display version information")
+      Term.(
+        const (fun () ->
+            print_endline ("STELF version " ^ version);
+            Fmt_tty.setup_std_outputs ();
+            Display.fmt Format.std_formatter @@ Pal.logo;
+            0)
+        $ const ())
+  in
+  let help_cmd : int Cmd.t =
+    Cmd.v
+      (Cmd.info "help" ~doc:"Display help information")
+      Term.(
+        const (fun () ->
+            print_endline ("STELF version " ^ version);
+            Fmt_tty.setup_std_outputs ();
+            Display.fmt Format.std_formatter @@ Pal.logo;
+            0)
+        $ const ()) (* TODO Make this work *)
+  in
+  let main_cmd =
+    Cmd.group
+      (Cmd.info "stelf" ~version ~doc:"The STELF proof assistant")
+      [ repl_cmd; check_cmd; version_cmd; help_cmd ]
+  in
+  Basis.OS.Process.exit (Cmd.eval' main_cmd)

doc/index.mld

@@ -3,59 +3,14 @@
 This is the internal docmentation for the STELF project. 
 
 {!modules:
-  Stelf
-  Cst 
-  Syntax 
-  Common
+  Common 
+  Cst
   Display
-  Error
+  Recon
+  Syntax
   Fronts
+  Pal 
+  Tui 
   IntSyn
   Lang
-  Recon
-  Compile
-  Compress
-  Cover
-  Debug
-  Domains
-  Flit
-  Formatter
-  Frontend
-  Global
-  Heuristic
-  Index
-  IntInf
-  Inverse
-  M2
-  Meta
-  Modes
-  Modules
-  Msg
-  Names
-  Netserver
-  Opsem
-  Order
-  Paths
-  Print
-  Prover
-  Server
-  Smlofnj
-  Solvers
-  Stream
-  Style
-  Subordinate
-  Table
-  Tabling
-  Terminate
-  Thm
-  Timing
-  Tomega
-  Trail
-  Typecheck
-  Unique
-  Worldcheck
-  Compile 
-  Compress
-  Cover
-  Display
 }