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

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

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 used by prologPages rocqPages

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"

used by prologPages

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

93prologPages=

pkgs.runCommand"filnix-prolog-pages" nativeBuildInputs = swipl;

mkdir -p $out

cp ${src}/nanofil/web/dterm.css ${src}/nanofil/web/dterm.js $out/

swipl ${src}/nanofil/web/dterm.pl $out ${src}/nanofil/src \

${lib.concatMapStringsSep" " d: "--doc=${src}/nanofil/docs/${d}.md" dtermDocs} \

--concepts=${src}/nanofil/docs/concepts --rocq=${src}/nanofil/rocq/theories \

--rocq=${src}/nanofil/rocq/spikes </dev/null

uses dtermDocs lib src swipl

103rocqPages=

pkgs.runCommand"filnix-rocq-pages" nativeBuildInputs = swipl;

mkdir -p $out

cp ${src}/nanofil/web/rocq/dterm-rocq.css ${src}/nanofil/web/rocq/dterm-rocq.js $out/

mapfile -t rocq < <(cd ${src} && find nanofil -name '*.v' | sort)

swipl ${src}/nanofil/web/rocq/dterm_rocq.pl $out ${src} \

--states=${proofStates} --states=${spikeStates} --prolog=${src}/nanofil/src \

--concepts=${src}/nanofil/docs/concepts "''${rocq[@]}" </dev/null

uses proofStates spikeStates src swipl

pkgs.runCommand"filnix-site"

116nativeBuildInputs=

pkgs.pandoc swipl

120passthru=

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