From c8a9b6cea69263b5e7f74bb7a3b75eaf35178920 Mon Sep 17 00:00:00 2001 From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com> Date: Thu, 26 Mar 2026 10:19:41 +0800 Subject: [PATCH] Move Candle specific files to a new subdirectory As explained in a comment in build-instructions.sh, this leads to a bit of changing directories at the beginning. The following mental model may be useful: all (relative) paths should be relative to the project root. The main wrinkle here is that the cake binary currently expects some files at hardcoded locations - so if we don't want those files to be at the top-level directory, we need to start Candle in a different location, and change directory right after booting. To enable this, we also make use of the new "custom" FFI port - this will become handy in the future for getting the time and calling external binaries. --- basics.ml | 2 +- build-instructions.sh | 36 ++++-- candle | 2 - candle.sh | 11 ++ candle/.gitignore | 1 + candle/basis_ffi.c.patch | 20 +++ cake.S.patch => candle/cake.S.patch | 0 candle/chdir_to_root.ml | 18 +++ candle_compute.ml => candle/compute.ml | 0 candle_insulate.py => candle/insulate.py | 0 candle_kernel.ml => candle/kernel.ml | 0 candle_nums.ml => candle/nums.ml | 0 candle_ocaml.ml => candle/ocaml.ml | 1 - candle_pretty.ml => candle/pretty.ml | 0 candle-regression.py => candle/regression.py | 49 ++++--- candletest | 16 --- candletest.mk | 128 ------------------- hol.ml | 6 - hol_lib.ml | 15 ++- test.sh | 2 +- 20 files changed, 120 insertions(+), 187 deletions(-) delete mode 100755 candle create mode 100755 candle.sh create mode 100644 candle/.gitignore create mode 100644 candle/basis_ffi.c.patch rename cake.S.patch => candle/cake.S.patch (100%) create mode 100644 candle/chdir_to_root.ml rename candle_compute.ml => candle/compute.ml (100%) rename candle_insulate.py => candle/insulate.py (100%) rename candle_kernel.ml => candle/kernel.ml (100%) rename candle_nums.ml => candle/nums.ml (100%) rename candle_ocaml.ml => candle/ocaml.ml (99%) rename candle_pretty.ml => candle/pretty.ml (100%) rename candle-regression.py => candle/regression.py (91%) delete mode 100755 candletest delete mode 100644 candletest.mk diff --git a/basics.ml b/basics.ml index 3647636f..dcb55220 100755 --- a/basics.ml +++ b/basics.ml @@ -8,7 +8,7 @@ (* (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018 *) (* ========================================================================= *) -needs "candle_kernel.ml";; +needs "candle/kernel.ml";; (* ------------------------------------------------------------------------- *) (* Create probably-fresh variable *) diff --git a/build-instructions.sh b/build-instructions.sh index 053508fe..cc071efc 100755 --- a/build-instructions.sh +++ b/build-instructions.sh @@ -1,32 +1,44 @@ #!/bin/bash +# Set up "strict mode" for bash set -euo pipefail +# Create (if needed) + Change into the build directory +mkdir -p candle/build +cd candle/build + # Get the 64-bit CakeML compiler from here: -curl -OL https://cakeml.org/regression/artefacts/3276/cake-x64-64.tar.gz -tar xvzf cake-x64-64.tar.gz +curl -OL https://cakeml.org/regression/artefacts/3286/cake-x64-64.tar.gz +tar xvzf cake-x64-64.tar.gz --strip-components=1 # By default, the CakeML compiler reserves a few kilobytes for constants and # code produced by the dynamic compiler. Using Candle requires setting these # to some megabytes: -patch cake-x64-64/cake.S cake.S.patch +patch cake.S ../cake.S.patch -# Build the compiler binary -cd cake-x64-64 && make && cd .. +# Patching in useful FFI calls +patch basis_ffi.c ../basis_ffi.c.patch -# Copy the compiler binary, the exported compiler state and candle_boot.ml into -# this directory: -cp cake-x64-64/cake cake-x64-64/config_enc_str.txt cake-x64-64/candle_boot.ml . +# Build the compiler binary +make # Create the types.txt file necessary for candle_insulate.py ./cake --types < /dev/null > types.txt 2>&1 # Generate candle_insulate.ml -python candle_insulate.py types.txt candle_insulate.ml +python ../insulate.py types.txt insulate.ml + +# The working directory of the binary will be CANDLE_ROOT/candle/build, +# so it needs to change directory to CANDLE_ROOT after booting.. +# +# Q: Why do we not start the cake binary from CANDLE_ROOT? +# A: The cake binary looks for config_enc_str.txt and candle_boot.ml relative +# to the current working directoy. I find it neater if these files are not +# copied to CANDLE_ROOT, but stay tucked away in the build folder. +# +cat ../chdir_to_root.ml >> candle_boot.ml # You can now run Candle by writing: -# $ ./cake --candle -# or: -# $ ./candle +# $ ./candle.sh # (without the $) at your prompt. Load the HOL Light sources by writing: # > #use "hol.ml";; # (without > and with double semicolons) in the REPL. diff --git a/candle b/candle deleted file mode 100755 index 774fb45f..00000000 --- a/candle +++ /dev/null @@ -1,2 +0,0 @@ -#!/bin/sh -./cake --candle diff --git a/candle.sh b/candle.sh new file mode 100755 index 00000000..057585e3 --- /dev/null +++ b/candle.sh @@ -0,0 +1,11 @@ +#!/bin/bash +# Set up "strict mode" for bash +set -euo pipefail + +# Change into correct directory - note that Candle must take care to change back +# to script_dir (see build-instructions.sh for more information) +script_dir=$(dirname -- "$(readlink -f -- "${BASH_SOURCE[0]}")") +cd $script_dir/candle/build + +# Start Candle +./cake --candle diff --git a/candle/.gitignore b/candle/.gitignore new file mode 100644 index 00000000..d1638636 --- /dev/null +++ b/candle/.gitignore @@ -0,0 +1 @@ +build/ \ No newline at end of file diff --git a/candle/basis_ffi.c.patch b/candle/basis_ffi.c.patch new file mode 100644 index 00000000..5b3720e3 --- /dev/null +++ b/candle/basis_ffi.c.patch @@ -0,0 +1,20 @@ +--- basis_ffi.c ++++ basis_ffi.c +@@ -294,6 +294,13 @@ + } + + void fficustom (unsigned char *c, long clen, unsigned char *a, long alen) { +- assert(0 <= alen); +- assert(0 <= clen); ++ if (strcmp(c, "chdir") == 0) { ++ assert(1 <= alen); ++ a[0] = chdir(a) != 0; ++ } else if (strcmp(c, "getcwd") == 0) { ++ assert(1 <= alen); ++ a[0] = getcwd(a + 1, alen - 1) == NULL; ++ } else { ++ return; ++ } + } + + // --------------------------------------------------------------------------- diff --git a/cake.S.patch b/candle/cake.S.patch similarity index 100% rename from cake.S.patch rename to candle/cake.S.patch diff --git a/candle/chdir_to_root.ml b/candle/chdir_to_root.ml new file mode 100644 index 00000000..abc3a6ca --- /dev/null +++ b/candle/chdir_to_root.ml @@ -0,0 +1,18 @@ + +exception Sys_error of string;; +let pp_exn e = + match e with + | Sys_error s -> + Pretty_printer.app_block "Sys_error" [Pretty_printer.pp_string s] + | _ -> pp_exn e;; + +let chdir dir = + let len = String.size dir in + let _ = if len = 0 then raise (Sys_error "Sys.chdir: empty input") else () in + let bytes = Word8_array.array (len + 1) (Word8.fromInt 0) in + let _ = Word8_array.copyVec dir 0 len bytes 0 in + let _ = Runtime.customFFI "chdir" bytes in + let ret = Word8.toInt (Word8_array.sub bytes 0) in + if ret <> 0 then raise (Sys_error "Sys.chdir: unsuccessful FFI") else ();; + +let _ = chdir "../..";; diff --git a/candle_compute.ml b/candle/compute.ml similarity index 100% rename from candle_compute.ml rename to candle/compute.ml diff --git a/candle_insulate.py b/candle/insulate.py similarity index 100% rename from candle_insulate.py rename to candle/insulate.py diff --git a/candle_kernel.ml b/candle/kernel.ml similarity index 100% rename from candle_kernel.ml rename to candle/kernel.ml diff --git a/candle_nums.ml b/candle/nums.ml similarity index 100% rename from candle_nums.ml rename to candle/nums.ml diff --git a/candle_ocaml.ml b/candle/ocaml.ml similarity index 99% rename from candle_ocaml.ml rename to candle/ocaml.ml index e3d4e932..fb2fac50 100644 --- a/candle_ocaml.ml +++ b/candle/ocaml.ml @@ -1,5 +1,4 @@ exception Invalid_argument of string;; -exception Sys_error of string;; exception End_of_file;; exception Not_found;; diff --git a/candle_pretty.ml b/candle/pretty.ml similarity index 100% rename from candle_pretty.ml rename to candle/pretty.ml diff --git a/candle-regression.py b/candle/regression.py similarity index 91% rename from candle-regression.py rename to candle/regression.py index 8a7a3ea7..2962c5c6 100644 --- a/candle-regression.py +++ b/candle/regression.py @@ -1,3 +1,21 @@ +""" +Simple Python script to test Candle. + +Note that this script assumes passwordless sudo for criu, which can be +achieved by: +1. Calling visudo +2. Adding + user ALL = (root) NOPASSWD: /usr/bin/criu + to it, taking care to replace user with the proper username. + +No claims are made on whether this a good idea in regards to security. + +The reason criu is used, is because DMTCP segfaulted on my machine. +However, I suspect that that might have been due to the packaged +version being outdated, so it is worth reconsidering, as it appears +that DMTCP supports one checkpoint to be restored multiple times +simulatenously, which would make parallelism during testing easier. +""" import sys import pexpect import time @@ -6,6 +24,10 @@ import argparse from dataclasses import dataclass from enum import Enum +from pathlib import Path + +# /candle/candle-regression.py +CANDLE_ROOT = Path(__file__).resolve().parent.parent # --------------------------------------------------------------------------- # Exceptions @@ -61,9 +83,9 @@ class TestResult: # --------------------------------------------------------------------------- class CandleREPL: - def __init__(self, base, restore=False): + def __init__(self, restore=False): # Easier to assume that we are in the candle directory for now. - os.chdir(base) + os.chdir(CANDLE_ROOT) # Indicates whether we are a restored instance. In that case, I suspect # that the pid of self.process might be of sudo criu restore instead of @@ -71,8 +93,7 @@ def __init__(self, base, restore=False): self._cake_pid = None self._logfile = sys.stdout - self._base = base - self._checkpoint_dir = "checkpoint" + self._checkpoint_dir = str(CANDLE_ROOT / "checkpoint") self._pidfile_name = "cake.pid" self.load_stack = [] @@ -82,7 +103,11 @@ def __init__(self, base, restore=False): self.restore() else: try: - self.process = pexpect.spawn("./candle", encoding='utf-8', logfile=self._logfile) + self.process = pexpect.spawn( + str(CANDLE_ROOT / "candle.sh"), + encoding='utf-8', + logfile=self._logfile + ) except Exception as e: raise StartFailure from e try: @@ -262,20 +287,19 @@ def print_summary(results): # --------------------------------------------------------------------------- class TestRunner: - def __init__(self, base_dir, timeout=600, fail_fast=False): - self.base_dir = base_dir + def __init__(self, timeout=600, fail_fast=False): self.timeout = timeout self.fail_fast = fail_fast def setup(self, reuse_checkpoint=False): """Start candle, load hol.ml, and dump a checkpoint.""" - checkpoint_path = os.path.join(self.base_dir, "checkpoint") + checkpoint_path = CANDLE_ROOT / "checkpoint" if reuse_checkpoint and os.path.isdir(checkpoint_path): print("Reusing existing checkpoint.") return print("Starting candle and loading hol.ml...") - repl = CandleREPL(self.base_dir) + repl = CandleREPL() try: repl.load("hol.ml", timeout=3600) print("hol.ml loaded. Dumping checkpoint...") @@ -290,7 +314,7 @@ def run_test(self, name): start = time.perf_counter() try: - repl = CandleREPL(self.base_dir, restore=True) + repl = CandleREPL(restore=True) except Exception as e: elapsed = time.perf_counter() - start return TestResult( @@ -401,10 +425,6 @@ def main(): "--timeout", type=int, default=600, help="Per-test timeout in seconds (default: 600)", ) - parser.add_argument( - "--base-dir", default=os.path.dirname(os.path.abspath(__file__)), - help="Candle base directory (default: script directory)", - ) args = parser.parse_args() @@ -422,7 +442,6 @@ def main(): tests = list(TESTS) runner = TestRunner( - base_dir=args.base_dir, timeout=args.timeout, fail_fast=args.fail_fast, ) diff --git a/candletest b/candletest deleted file mode 100755 index 63638db0..00000000 --- a/candletest +++ /dev/null @@ -1,16 +0,0 @@ -#!/bin/bash -####################################################################### -# Load in a bunch of examples to test Candle is working properly -# See candletest.mk on details on how to set it up. -# -# Try examining the output using something like -# -# grep -E '###|ERROR|EXCEPTION|TIMEOUT|failure|Parsing failed|error in|not.found' /tmp/candle-test/candletest.log -# -# to see progress and whether anything has gone wrong. -# -####################################################################### - -set -e - -make SHELL=bash -f candletest.mk all diff --git a/candletest.mk b/candletest.mk deleted file mode 100644 index 39c06ee7..00000000 --- a/candletest.mk +++ /dev/null @@ -1,128 +0,0 @@ -# I assume a snapshot with hol.ml loaded was made using criu (which only works -# with Linux, sorry). -# -# You can create such a snapshot by following: -# 1. Start candle normally in a terminal -# 2. Manually load hol.ml using #use "hol.ml";; -# 3. Wait until loading is done -# 4. Make sure you are in the candle repositry, and an (empty) directory called -# checkpoint exists (I am not sure whether it has to be empty, but just to -# be sure...) -# 5. Run sudo criu dump -D checkpoint -t $(pidof cake) --shell-job -# If you look at the terminal where Candle was running, it should have been -# killed. If not, maybe you got the wrong cake process? -# -# criu might complain about a lack of capabilities. In that case, you should -# consult your preferred resources to find out how you can give those -# CAP_SYS_ADMIN to it. - -# To restore, we can use the following command: -# sudo criu restore -D checkpoint/ --shell-job - -# Since we need to restore into a terminal, but also want to call it via make -# we need to place it into a pseudoterminal. To avoid having to somehow pass -# the user password into that, we assume that criu can be run with sudo without -# a password. -# -# This can be achieved by: -# 1. Calling visudo -# 2. Adding -# user ALL = (root) NOPASSWD: /usr/bin/criu -# to it, taking care to replace user with the proper username. -# -# No claims are made on whether this a good idea in regards to security. - -# The above procedure is a bit hacky, so if anyone knows a better way, please -# let me know. - -# In some cases, Ctrl-C may not be enough to stop the tests. In that case, -# kill the process (for example using pkill cake). - -# To rerun the tests, you need to remove the directory specified in LOGDIR -# (see below). - -CANDLE:=python3 -c "import pty,sys; pty.spawn(['sudo','criu','restore','-D','checkpoint/','--shell-job'])" - -GREAT_100_THEOREMS:= \ - 100/arithmetic_geometric_mean \ - 100/arithmetic \ - 100/ballot \ - 100/bernoulli \ - 100/bertrand \ - 100/birthday \ - 100/cantor \ - 100/cayley_hamilton \ - 100/ceva \ - 100/circle \ - 100/chords \ - 100/combinations \ - 100/constructible \ - 100/cosine \ - 100/cubic \ - 100/derangements \ - 100/desargues \ - 100/descartes \ - 100/dirichlet \ - 100/div3 \ - 100/divharmonic \ - 100/e_is_transcendental \ - 100/euler \ - 100/feuerbach \ - 100/fourier \ - 100/four_squares \ - 100/friendship \ - 100/fta \ - 100/gcd \ - 100/heron \ - 100/inclusion_exclusion \ - 100/independence \ - 100/isoperimetric \ - 100/isosceles \ - 100/konigsberg \ - 100/lagrange \ - 100/leibniz \ - 100/lhopital \ - 100/liouville \ - 100/minkowski \ - 100/morley \ - 100/pascal \ - 100/perfect \ - 100/pick \ - 100/piseries \ - 100/platonic \ - 100/pnt \ - 100/polyhedron \ - 100/primerecip \ - 100/ptolemy \ - 100/pythagoras \ - 100/quartic \ - 100/ramsey \ - 100/ratcountable \ - 100/realsuncountable \ - 100/reciprocity \ - 100/sqrt \ - 100/stirling \ - 100/subsequence \ - 100/thales \ - 100/transcendence \ - 100/triangular \ - 100/two_squares \ - 100/wilson - -TESTS:=$(GREAT_100_THEOREMS) - -LOGDIR:=/tmp/candle-test - -LOGS:=$(patsubst %,$(LOGDIR)/%,$(TESTS)) - -READY:=$(patsubst %,%.ready,$(LOGS)) - -all: $(READY) - cat $(LOGS) > $(LOGDIR)/candletest.log - -$(LOGDIR)/%.ready: - @mkdir -p $(LOGDIR)/$$(dirname $*) - @echo '### Loading $*.ml' - @echo '### Loading $*.ml' > $(LOGDIR)/$* - @echo 'loads "$*.ml";;Cake.Runtime.exit 0;;' | ($(CANDLE) >> $(LOGDIR)/$* 2>&1) || echo "TIMEOUT" >> $(LOGDIR)/$* - @touch $(LOGDIR)/$*.ready diff --git a/hol.ml b/hol.ml index 83fc5e3d..398c4c10 100644 --- a/hol.ml +++ b/hol.ml @@ -63,12 +63,6 @@ let set_color_printer (use_color:bool) = set_color_printer true;; *) -(* ------------------------------------------------------------------------- *) -(* In-logic computation function. *) -(* ------------------------------------------------------------------------- *) - -loads "candle_compute.ml";; (* Definitions of cval primitives *) - (* ------------------------------------------------------------------------- *) (* The help system. *) (* ------------------------------------------------------------------------- *) diff --git a/hol_lib.ml b/hol_lib.ml index 2270e999..bd9ed5a9 100644 --- a/hol_lib.ml +++ b/hol_lib.ml @@ -20,10 +20,10 @@ open Hol_loader;; (* compatiblity layer. *) (* ------------------------------------------------------------------------- *) -loads "candle_insulate.ml";; (* Auto-generated. Moves CakeML specifics. *) -loads "candle_nums.ml";; (* Load "num". *) -loads "candle_pretty.ml";; (* Pretty printer code. *) -loads "candle_ocaml.ml";; (* OCaml modules. *) +loads "candle/build/insulate.ml";; (* Moves CakeML specifics. *) +loads "candle/nums.ml";; (* Load "num". *) +loads "candle/pretty.ml";; (* Pretty printer code. *) +loads "candle/ocaml.ml";; (* OCaml modules. *) (* ------------------------------------------------------------------------- *) (* Bind these to names that are independent of OCaml versions before they *) @@ -49,7 +49,7 @@ loads "lib.ml";; (* Various useful general library functions *) (* Candle things. *) (* ------------------------------------------------------------------------- *) -loads "candle_kernel.ml";; (* Brings Candle kernel into scope. *) +loads "candle/kernel.ml";; (* Brings Candle kernel into scope. *) (* ------------------------------------------------------------------------- *) (* Some extra support stuff needed outside the core. *) @@ -116,6 +116,11 @@ loads "iterate.ml";; (* Iterated operations *) loads "cart.ml";; (* Finite Cartesian products *) loads "define.ml";; (* Support for general recursive definitions *) +(* ------------------------------------------------------------------------- *) +(* In-logic computation function. *) +(* ------------------------------------------------------------------------- *) + +loads "candle/compute.ml";; (* Definitions of cval primitives *) (* ------------------------------------------------------------------------- *) (* Checks that no axiom other than those allowed by core libs are introduced *) diff --git a/test.sh b/test.sh index dd3d64a8..5a09811f 100755 --- a/test.sh +++ b/test.sh @@ -5,4 +5,4 @@ set -euo pipefail ./build-instructions.sh # Run regression suite -python candle-regression.py \ No newline at end of file +python candle/regression.py