Fil-C on Nix

Filnix wiki

mbrock/filnix

packages/site/default.nix

The GitHub Pages site: pages/ as is, docs/ rendered with pandoc into docs/*.html, nanofil's Prolog drawn as terms into nanofil/*.html by nanofil/web/dterm.pl, nanofil's Rocq into nanofil/rocq/*.html by nanofil/web/rocq, nanofil's documents into nanofil/*.html (dterm) or nanofil/docs/*.html (pandoc), with its README as nanofil/index.html, the nanofil playground in nanofil/play/, and every Nix file of filnix drawn by dterm-nix into nix/*.html. .github/workflows/pages.yml publishes it.

λpkgs, filcc, filnix, nixpkgs
let

For the option index: the flake's modules, and Nixpkgs' NixOS.

17inherit pkgs
lib

One SWI-Prolog for the dterm pages, the playground's build and the playground in the browser (swipl-wasm is 10.1.19).

20swipl=
import../../nanofil/web/play/swipl.nix inherit pkgs;
used by prologPages rocqPages
21play=
import../../nanofil/web/play inherit pkgs filcc swipl;
22proofStates=
import../../nanofil/web/rocq/capture.nix inherit pkgs;
used by rocqPages

The logic spikes' states, with Iris; only the site depends on them.

24spikeStates=
import../../nanofil/web/rocq/capture.nix
25inherit
pkgs
26spikes=
true
used by rocqPages

The Nix files drawn as pages (dterm-nix): every Nix file of the repository, but for the trees that are not filnix's own Nix: build results (result*) and experiments/, scratch projects with their own flakes. One that does not parse fails the build. The repository's paths are listed for the links of the others.

33rel=
f: lib.removePrefix"./" lib.path.removePrefix../.. f
uses lib used by nixPages repoFiles
34drawn=
λf
let
37parts=
lib.splitString"/" f
uses lib
in
lib.headparts ≢ "experiments" ∧ ¬lib.anylib.hasPrefix"result" parts
uses lib used by nixPages
40nixPages=
lib.filterdrawn maprel lib.fileset.toListlib.fileset.fileFilterf: f.hasExt"nix" ../..
uses drawn lib rel used by src
45repoFiles=
builtins.toFile"filnix-files" lib.concatMapStringsf: relf + "\n" lib.fileset.toList../..
uses lib rel

The option index of the NixOS and finix modules, from evaluating them (dterm-nix/options.nix), as JSON.

50options=
builtins.toFile"filnix-options.json"
builtins.toJSON
import../../dterm-nix/options.nix
53inherit
lib
54evalNixos=
λmodules
import"${nixpkgs}/nixos/lib/eval-config.nix"
57inherit pkgs.stdenv.hostPlatform
system
58inherit
modules
60inherit
filnix pkgs
61nixpkgsRoot=
nixpkgs
62nixpkgsRev=
nixpkgs.rev or "master"
66src=
lib.fileset.toSource
67root=
../..
68fileset=
lib.fileset.unions
../../docs
../../pages
../../nanofil/docs
../../nanofil/src
../../nanofil/web

nanofil's Rocq, wherever the development puts it (dterm-rocq).

lib.fileset.fileFilterf: f.hasExt"v" ../../nanofil
../../dterm-nix
lib.fileset.unionsmapf: ../.. + "/${f}" nixPages
uses lib nixPages

nanofil's documents dterm draws beside the modules, at nanofil/NAME.html, with concept, module and Rocq links; README is nanofil's home page, nanofil/index.html. pandoc renders the others into nanofil/docs.

83dtermDocs=
"README" "guide" "formal" "filc" "iris" "logic" "nfb-guide-argon" "nfb-guide-wonder" "nfb-guide-wonderful"
used by prologPages

dterm reads Prolog, concepts, saved guide outputs and Rocq indexes. Keep nanofil/docs for its document-link existence checks as well as the rendered documents, but not unrelated site docs/pages/Nix.

The Rocq pages read the complete Rocq/Prolog/concept index, but not ordinary Markdown or the rest of the website. Keep those edits from invalidating the cached rendering as well as the proof captures.

Independent renderers are cached separately. The Rocq invocation still sees every source for its real cross-file index and captured states.

132prologPages=
pkgs.runCommand"filnix-prolog-pages" nativeBuildInputs = swipl;
mkdir -p $out
cp ${prologSrc}/nanofil/web/dterm.css ${prologSrc}/nanofil/web/dterm.js $out/
swipl ${prologSrc}/nanofil/web/dterm.pl $out ${prologSrc}/nanofil/src \
${lib.concatMapStringsSep" " d: "--doc=${prologSrc}/nanofil/docs/${d}.md" dtermDocs} \
--concepts=${prologSrc}/nanofil/docs/concepts --rocq=${prologSrc}/nanofil/rocq/theories \
--rocq=${prologSrc}/nanofil/rocq/spikes --rocq=${prologSrc}/nanofil/rocq/backend \
--rocq=${prologSrc}/nanofil/rocq/glibc </dev/null
uses dtermDocs lib prologSrc swipl
147rocqPages=
pkgs.runCommand"filnix-rocq-pages" nativeBuildInputs = swipl;
mkdir -p $out
cp ${rocqSrc}/nanofil/web/rocq/dterm-rocq.css ${rocqSrc}/nanofil/web/rocq/dterm-rocq.js $out/
mapfile -t rocq < <(cd ${rocqSrc} && find nanofil -name '*.v' | sort)
swipl ${rocqSrc}/nanofil/web/rocq/dterm_rocq.pl $out ${rocqSrc} \
--states=${proofStates} --states=${spikeStates} --prolog=${rocqSrc}/nanofil/src \
--concepts=${rocqSrc}/nanofil/docs/concepts "''${rocq[@]}" </dev/null
uses proofStates rocqSrc spikeStates swipl
in
pkgs.runCommand"filnix-site"
160nativeBuildInputs=
pkgs.pandoc swipl
164passthru=
inherit play proofStates spikeStates prologPages rocqPages;
export PROLOG_PAGES=${prologPages} ROCQ_PAGES=${rocqPages} \
DTERM_DOCS=${lib.escapeShellArgtoStringdtermDocs}
bash ${./.}/build.sh ${src} $out ${repoFiles} ${options} ${nixpkgs} \
${lib.escapeShellArgsnixPages}
cp -r ${play} $out/nanofil/play