Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ jobs:
strategy:
fail-fast: false
matrix:
os: [ubuntu-latest, macos-latest]
os: [ubuntu-latest, macos-latest, windows-latest]
browser: [electron, chrome]
steps:
- name: Checkout repository
Expand Down
22 changes: 22 additions & 0 deletions Projects/MathlibDemo/build.cmd
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
REM @echo off
setlocal enabledelayedexpansion

REM Operate in the directory where this file is located
cd /d "%~dp0"

REM Updating Mathlib: We follow the instructions at
REM https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency#updating-mathlib4

REM Note: we had once problems with the `lake-manifest` when a new dependency got added
REM to `mathlib`, we may need to add `rm lake-manifest.json` again if that's still a problem.

REM currently the mathlib post-update-hook is not good enough to update the lean-toolchain.
REM things break if the new lakefile is not valid in the old lean version
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

REM note: mathlib has now a post-update hook that modifies the `lean-toolchain`
REM and calls `lake exe cache get`.

lake update -R
lake build
lake build Batteries
21 changes: 0 additions & 21 deletions Projects/MathlibDemo/build.sh

This file was deleted.

File renamed without changes.
8 changes: 8 additions & 0 deletions Projects/Stable/build.cmd
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
@echo off
setlocal enabledelayedexpansion

REM Operate in the directory where this file is located
cd /d "%~dp0"

lake update -R
lake build
20 changes: 20 additions & 0 deletions package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

15 changes: 8 additions & 7 deletions package.json
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@
],
"scripts": {
"start": "concurrently -n server,client -c blue,green \"npm run start:server\" \"npm run start:client\"",
"start:server": "cd server && NODE_ENV=development nodemon ./index.mjs",
"start:client": "NODE_ENV=development vite --host",
"start:server": "cd server && cross-env NODE_ENV=development nodemon ./index.mjs",
"start:client": "cross-env NODE_ENV=development vite --host",
"build": "npm run build:server && npm run build:client",
"build:server": "server/build.sh",
"build:client": "tsc -b && NODE_ENV=production vite build",
"production": "NODE_ENV=production node server/index.mjs",
"build:server": "node server/build.cjs",
"build:client": "tsc -b && cross-env NODE_ENV=production vite build",
"production": "cross-env NODE_ENV=production node server/index.mjs",
"dev": "vite",
"lint": "eslint . --ext ts,tsx --report-unused-disable-directives --max-warnings 0",
"preview": "vite preview",
Expand Down Expand Up @@ -55,6 +55,7 @@
"@types/react": "^19.0.10",
"@types/react-dom": "^19.0.4",
"@vitejs/plugin-react-swc": "^3.8.0",
"cross-env": "^7.0.3",
"cypress": "^13.17.0",
"cypress-iframe": "^1.0.1",
"cypress-real-events": "^1.14.0",
Expand All @@ -65,7 +66,7 @@
"vite-plugin-svgr": "^4.3.0",
"wait-on": "^8.0.2"
},
"engines" : {
"node" : ">=22.0.0"
"engines": {
"node": ">=22.0.0"
}
}
44 changes: 44 additions & 0 deletions server/build.cjs
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
#!/usr/bin/env node

const fs = require('fs');
const path = require('path');
const { spawnSync } = require('child_process');

// Change to ../Projects directory relative to this script
const baseDir = path.resolve(__dirname, '../Projects');
process.chdir(baseDir);
const isWin = process.platform === 'win32';
const buildScriptName = isWin ? 'build.cmd' : 'build.sh';

// Iterate over subfolders in Projects
fs.readdirSync('.').forEach(folder => {
const folderPath = path.join(baseDir, folder);

if (fs.lstatSync(folderPath).isDirectory()) {

const buildScriptPath = path.join(folderPath, buildScriptName);

if (fs.existsSync(buildScriptPath)) {
const start = Date.now();

console.log(`Start building ${folder}`);
if (!isWin) {
spawnSync('logger', ['-t', 'lean4web', `Start building ${folder}`]);
}

// Run the build script
const result = spawnSync('bash', [buildScriptPath], { stdio: 'inherit' });

const duration = Math.floor((Date.now() - start) / 1000);
const minutes = Math.floor(duration / 60);
const seconds = duration % 60;

console.log(`Finished ${folder} in ${minutes}:${seconds < 10 ? '0' : ''}${seconds} min`);
if (!isWin) {
spawnSync('logger', ['-t', 'lean4web', `Finished ${folder} in ${minutes}:${seconds < 10 ? '0' : ''}${seconds} min`]);
}
} else {
console.log(`Skipping ${folder}: ${buildScriptName} missing`);
}
}
});
24 changes: 0 additions & 24 deletions server/build.sh

This file was deleted.

Loading