Skip to content

Commit a339ca7

Browse files
committed
site: update agda docs
1 parent 9957634 commit a339ca7

File tree

1,097 files changed

+643107
-124050
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,097 files changed

+643107
-124050
lines changed

site/agda-docs.config.json

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{
2+
"backButtonUrl": "/formal-spec/",
3+
"inputDir": "./static/formal-spec",
4+
"modules": ["Leios", "Cardano", "Ouroboros", "Ledger", "Ledger-Spec"],
5+
"githubUrl": "https://github.com/input-output-hk/ouroboros-leios-formal-spec",
6+
"searchGranularity": "comprehensive"
7+
}

site/package.json

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@
1212
"serve": "docusaurus serve",
1313
"write-translations": "docusaurus write-translations",
1414
"write-heading-ids": "docusaurus write-heading-ids",
15-
"typecheck": "tsc"
15+
"typecheck": "tsc",
16+
"build-agda-docs": "bash scripts/build-and-process-agda-docs.sh"
1617
},
1718
"dependencies": {
1819
"@docusaurus/core": "3.4.0",
@@ -22,7 +23,8 @@
2223
"prism-react-renderer": "^2.3.0",
2324
"react": "^18.0.0",
2425
"react-dom": "^18.0.0",
25-
"undici": "^7.2.3"
26+
"undici": "^7.2.3",
27+
"agda-web-docs-lib": "^0.3.1"
2628
},
2729
"devDependencies": {
2830
"@docusaurus/module-type-aliases": "3.4.0",

site/scripts/build-agda-docs.sh

Lines changed: 0 additions & 23 deletions
This file was deleted.
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
#!/bin/bash
2+
3+
# Exit on error
4+
set -e
5+
6+
# Get the absolute paths
7+
SITE_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
8+
FORMAL_SPEC_DIR="$SITE_DIR/static/formal-spec"
9+
FORMAL_SPEC_ROOT="$(cd "$SITE_DIR/../../ouroboros-leios-formal-spec" && pwd)"
10+
11+
echo "Building Agda documentation..."
12+
13+
# Build Agda documentation
14+
(cd "$FORMAL_SPEC_ROOT" && nix build .#leiosDocs)
15+
16+
# Create formal-spec directory if it doesn't exist and set permissions
17+
mkdir -p "$FORMAL_SPEC_DIR"
18+
chmod 755 "$FORMAL_SPEC_DIR"
19+
20+
# Remove existing files if any
21+
rm -rf "$FORMAL_SPEC_DIR"/*
22+
23+
# Copy files with proper permissions (macOS compatible)
24+
cp -R "$FORMAL_SPEC_ROOT/result/html/"* "$FORMAL_SPEC_DIR/"
25+
chmod -R 755 "$FORMAL_SPEC_DIR"
26+
27+
echo "Processing HTML files..."
28+
29+
# Check if config file exists
30+
CONFIG_PATH="$SITE_DIR/agda-docs.config.json"
31+
if [ ! -f "$CONFIG_PATH" ]; then
32+
echo "Error: agda-docs.config.json not found"
33+
exit 1
34+
fi
35+
36+
# Process HTML files using the agda-web-docs-lib
37+
cd "$SITE_DIR" && NODE_OPTIONS="--max-old-space-size=16384" npx agda-web-docs-lib process "$FORMAL_SPEC_DIR" "$CONFIG_PATH"

site/scripts/dev-with-formal-spec.sh

Lines changed: 0 additions & 43 deletions
This file was deleted.

0 commit comments

Comments
 (0)