test new workflow with dockerfile

.github/workflows/build.yml

@@ -7,82 +7,101 @@ on:
   pull_request:
     branches: ["main"]
 jobs:
-  start-server:
-    name: Start server
-    runs-on: ubuntu-latest
-    # outputs:
-    #   server-url: ${{ steps.server-output.outputs.server-url }}
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          submodules: true
-      - uses: actions/setup-node@v4
-      - uses: leanprover/lean-action@v1
-        with:
-          lake-package-directory: "demo/server/LeanProject"
-          use-mathlib-cache: false
-          auto-config: false
-          build: true
-          test: false
-          lint: false
-      - name: Install dependencies
-        run: npm install
-      - name: Install demo
-        run: npm run setup_demo
-      # - name: Build lean4monaco
-      #   run: npm run build
-      # - name: Build demo server
-      #   run: |
-      #     cd demo
-      #     npm run build
-      - name: Start server
-        id: start-server
-        run: |
-          nohup npm start > nohup.out 2> nohup.err < /dev/null &
-          echo "server is running..."
-# cd demo
-# echo "Starting server..."
-# npm run start
-# # nohup npm run start > nohup.out 2> nohup.err < /dev/null &
-# echo "server is running."
   test:
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-          - name: Linux
-            os: ubuntu-latest
-          # - name: macOS
-          #   os: macos-latest
-          - name: Windows
-            os: windows-latest
-    name: ${{ matrix.name }}
-    runs-on: ${{ matrix.os }}
-    needs: start-server
+    runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
         with:
           submodules: true
-      - uses: actions/setup-node@v4
-      - name: Install dependencies
-        run: npm install
-      # - name: Wait for server
-      #   run: |
-      #     echo "Pinging the server to check if it's up..."
-      #     for i in {1..30}; do
-      #       curl -sSf http://localhost:5173 && break
-      #       echo "Waiting for server..."
-      #       sleep 5
-      #     done
-      # - name: Run Cypress tests
-      #   run: |
-      #     # wait-on http://localhost:5173
-      #     cypress run
-
-      #     #       # Install npm dependencies, cache them correctly
-      # and run all Cypress tests
+      - name: build docker image
+        run: docker build -t hhu-adam/lean4monaco .
+      - name: start server
+        run: docker run -dit -p 5173:5173 -p 8080:8080 hhu-adam/lean4monaco
       - name: Run tests
         uses: cypress-io/github-action@v6
-        # with:
+        with:
+          browser: chrome
         #   start: npm start
-        #   wait-on: 'http://localhost:5173'
+          wait-on: 'http://localhost:5173'
+
+
+#   start-server:
+#     name: Start server
+#     runs-on: ubuntu-latest
+#     # outputs:
+#     #   server-url: ${{ steps.server-output.outputs.server-url }}
+#     steps:
+#       - uses: actions/checkout@v4
+#         with:
+#           submodules: true
+#       - uses: actions/setup-node@v4
+#       - uses: leanprover/lean-action@v1
+#         with:
+#           lake-package-directory: "demo/server/LeanProject"
+#           use-mathlib-cache: false
+#           auto-config: false
+#           build: true
+#           test: false
+#           lint: false
+#       - name: Install dependencies
+#         run: npm install
+#       - name: Build and setup demo
+#         run: npm run setup_demo
+#       # - name: Build lean4monaco
+#       #   run: npm run build
+#       # - name: Build demo server
+#       #   run: |
+#       #     cd demo
+#       #     npm run build
+#       - name: Start server
+#         id: start-server
+#         run: |
+#           nohup npm start > nohup.out 2> nohup.err < /dev/null &
+#           echo "server is running..."
+# # cd demo
+# # echo "Starting server..."
+# # npm run start
+# # # nohup npm run start > nohup.out 2> nohup.err < /dev/null &
+# # echo "server is running."
+#   test:
+#     strategy:
+#       fail-fast: false
+#       matrix:
+#         include:
+#           - name: Linux
+#             os: ubuntu-latest
+#           # - name: macOS
+#           #   os: macos-latest
+#           - name: Windows
+#             os: windows-latest
+#     name: ${{ matrix.name }}
+#     runs-on: ${{ matrix.os }}
+#     needs: start-server
+#     steps:
+#       - uses: actions/checkout@v4
+#         with:
+#           submodules: true
+#       - uses: actions/setup-node@v4
+#       - name: Install dependencies
+#         run: npm install
+#       # - name: Wait for server
+#       #   run: |
+#       #     echo "Pinging the server to check if it's up..."
+#       #     for i in {1..30}; do
+#       #       curl -sSf http://localhost:5173 && break
+#       #       echo "Waiting for server..."
+#       #       sleep 5
+#       #     done
+#       # - name: Run Cypress tests
+#       #   run: |
+#       #     # wait-on http://localhost:5173
+#       #     cypress run
+
+#       #     #       # Install npm dependencies, cache them correctly
+#       # and run all Cypress tests
+#       - name: Run tests
+#         uses: cypress-io/github-action@v6
+#         with:
+#           browser: chrome
+#         #   start: npm start
+#         #   wait-on: 'http://localhost:5173'

Dockerfile

@@ -0,0 +1,32 @@
+FROM node:20
+
+USER root
+
+RUN mkdir project
+WORKDIR /project
+
+COPY . /project
+
+## TODO: Are these necessary to avoid local artifacts copied inside the container?
+RUN rm -rf node_modules
+RUN rm -rf demo/node_modules
+RUN rm -rf demo/server/node_modules
+RUN rm -rf dist
+RUN rm -rf demo/dist
+
+# Install Lean/elan
+ENV ELAN_HOME=/usr/local/elan \
+  PATH=/usr/local/elan/bin:$PATH
+RUN export LEAN_VERSION="$(cat /project/demo/server/LeanProject/lean-toolchain)" && \
+  curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --no-modify-path --default-toolchain $LEAN_VERSION; \
+    chmod -R a+w $ELAN_HOME; \
+    elan --version; \
+    lean --version; \
+    leanc --version; \
+    lake --version;
+
+# Install the demo project
+RUN npm install
+RUN npm run setup_demo
+
+CMD ["npm", "start"]

README.md

@@ -174,6 +174,7 @@ Afterwards, you can run the demo with
 ```
 cd lean4monaco
 npm install
+npm setup_demo # this builds lean4monaco and calls `npm install` in `demo/`
 npm start
 ```
 

package.json

@@ -34,7 +34,7 @@
   },
   "scripts": {
     "setup_demo": "concurrently \"(cd demo && npm install)\" \"npm run build\" -n install,build -c \"bgCyan.bold,bgBlue.bold\"",
-    "start": "npm run setup_demo && concurrently \"tsc -w --preserveWatchOutput\" \"webpack --watch\" \"npm run watch:copyfiles\" \"cd demo && npm run start_client\" \"cd demo && npm run start_server\" -n tsc,webpack,copyfiles,vite,server -c \"bgGreen.bold,bgBlue.bold,bgCyan.bold,bgYellow.bold,bgMagenta.bold\"",
+    "start": "concurrently \"tsc -w --preserveWatchOutput\" \"webpack --watch\" \"npm run watch:copyfiles\" \"cd demo && npm run start_client\" \"cd demo && npm run start_server\" -n tsc,webpack,copyfiles,vite,server -c \"bgGreen.bold,bgBlue.bold,bgCyan.bold,bgYellow.bold,bgMagenta.bold\"",
     "watch:copyfiles": "nodemon --watch ./src --exec \"npm run build:copyfiles\"",
     "build:copyfiles": "cd src && copyfiles \"**/*.json\" \"**/*.css\" \"**/*.ttf\" \"**/*.otf\" \"**/*.svg\" ../dist/",
     "build": "tsc && webpack && npm run build:copyfiles",