Skip to content

Commit

Permalink
udpate workflows
Browse files Browse the repository at this point in the history
  • Loading branch information
@joneugster
joneugster committed Aug 24, 2024
1 parent c5640e6 commit d8017f8
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 247 deletions.
219 changes: 6 additions & 213 deletions .github/workflows/docker.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,15 @@ run-name: Test docker image
on:
workflow_dispatch:
push:
branches: ["main"] # replace "main" with the default branch
branches: ["main"]
pull_request:
branches: ["main"]
concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true
defaults:
run:
shell: bash
jobs:
build:
name: 'Build image'
Expand Down Expand Up @@ -37,51 +40,14 @@ jobs:
path: /tmp/lean4monaco.tar
test:
needs: build
# # 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 }}
name: Test image
runs-on: 'ubuntu-latest'
steps:
- uses: actions/checkout@v4
with:
submodules: true
# - uses: leanprover/lean-action@v1
# if: matrix.os != 'windows-latest'
# with:
# lake-package-directory: "demo/server/LeanProject"
# use-mathlib-cache: false
# auto-config: false
# build: true
# test: false
# lint: false
# - name: Install elan (Windows)
# if: matrix.os == 'windows-latest'
# run: |
# curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh
# bash elan-init.sh -y
# echo "$(realpath ~/.elan/bin)" >> $GITHUB_PATH
# shell: bash
# - name: Run lake build (Windows)
# if: matrix.os == 'windows-latest'
# run: |
# cd demo/server/LeanProject
# lake build
# shell: bash
- name: Install dependencies
run: npm install
# - name: Build
# run: npm run build
# - run: npm run setup_demo
- name: Download server image
uses: actions/download-artifact@v4
with:
Expand All @@ -91,181 +57,8 @@ jobs:
run: docker load --input /tmp/lean4monaco.tar
- name: Start server
run: docker run -dit -p 5173:5173 -p 8080:8080 lean4monaco
- name: Run tests
- name: Run tests (electron)
uses: cypress-io/github-action@v6
with:
# browser: chrome
# start: npm start
browser: electron
wait-on: 'http://localhost:5173'
# test:
# strategy:
# fail-fast: false
# matrix:
# include:
# - name: Linux
# os: ubuntu-latest
# - name: macOS
# os: macos-latest
# - name: Windows
# os: windows-latest
# runs-on: ubuntu-latest
# steps:
# - uses: actions/checkout@v4
# with:
# submodules: true
# - 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:
# browser: chrome
# # start: npm start
# 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'



# name: Test
# run-name: Test editor end-to-end
# on:
# workflow_dispatch:
# push:
# branches: ["main"] # replace "main" with the default branch
# pull_request:
# branches: ["main"]
# concurrency:
# group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
# cancel-in-progress: true
# jobs:
# 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 }}
# steps:
# - uses: actions/checkout@v4
# with:
# submodules: true
# - uses: leanprover/lean-action@v1
# if: matrix.os != 'windows-latest'
# with:
# lake-package-directory: "demo/server/LeanProject"
# use-mathlib-cache: false
# build: true
# test: false
# lint: false
# - name: Install elan (Windows)
# if: matrix.os == 'windows-latest'
# run: |
# curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh
# bash elan-init.sh -y
# echo "$(realpath ~/.elan/bin)" >> $GITHUB_PATH
# shell: bash
# - name: Run lake build (Windows)
# if: matrix.os == 'windows-latest'
# run: |
# cd demo/server/LeanProject
# lake build
# shell: bash
# - uses: actions/setup-node@v4
# # Install npm dependencies, cache them correctly
# # and run all Cypress tests
# - name: Run tests
# uses: cypress-io/github-action@v6
# with:
# start: npm start
# wait-on: 'http://localhost:5173'
# - run: npm audit
# if: matrix.os == 'ubuntu-latest'
# continue-on-error: true
29 changes: 7 additions & 22 deletions .github/workflows/test.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,9 @@ on:
concurrency:
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true
defaults:
run:
shell: bash
jobs:
test:
strategy:
Expand All @@ -25,23 +28,23 @@ jobs:
- chrome
- firefox
- webkit
experimental:
- false
include:
- os: ubuntu-latest
name: Linux
- os: macos-latest
name: macOS
- os: windows-latest
name: Windows
- os: windows-latest
name: Windows
browser: edge
exclude:
- os: windows-latest
browser: webkit

name: ${{ matrix.name }} - ${{ matrix.browser }}
runs-on: ${{ matrix.os }}
# Windows server is not working yet
continue-on-error: ${{ matrix.os == 'windows-latest' || matrix.browser == 'webkit' }}
continue-on-error: ${{ matrix.os == 'windows-latest' }} # add exceptions for failing jobs here
steps:
- name: Setup firefox (macOS)
if: matrix.os == 'macos-latest' && matrix.browser == 'firefox'
Expand All @@ -67,30 +70,12 @@ jobs:
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh
bash elan-init.sh -y
echo "$(realpath ~/.elan/bin)" >> $GITHUB_PATH
shell: bash
- uses: actions/setup-node@v4
- run: npm install
shell: bash
- run: npm run setup_demo
shell: bash
# # BUG: Somehow `lake` is not found when called through `npm` but it works on its own
# - name: Run npm run setup_demo (Windows)
# if: matrix.os == 'windows-latest'
# run: |
# npm run build
# cd demo
# npm install
# cd server/LeanProject
# lake build
# shell: bash

- name: Run tests
uses: cypress-io/github-action@v6
with:
start: npm start
wait-on: 'http://localhost:5173'
browser: ${{ matrix.browser }}
# - run: npm audit
# if: matrix.os == 'ubuntu-latest'
# continue-on-error: true

11 changes: 0 additions & 11 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -207,17 +207,6 @@ npm run test

for the automated cypress tests.

### OS support

Currently there is no support for Windows servers!

However, we do actively support Windows clients (i.e. browsers) accessing the website hosted
on a Linux machine! (unfortunately the github workflow does not test this)

There is a Linux Dockerfile which you might find useful to get
it running on a Windows machine (see below), but be advised you might need to
invest some time and effort if you're trying to set up a Windows server…

### Docker image

The Dockerfile defines an image where the server is run in a Linux container.
Expand Down
2 changes: 1 addition & 1 deletion cypress.config.ts
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import { defineConfig } from "cypress";

export default defineConfig({
defaultCommandTimeout: 10000,
defaultCommandTimeout: 40000, // default timeout was 4000. Infoview loading is slow on Windows...
experimentalWebKitSupport: true,
e2e: {
setupNodeEvents(on, config) {
Expand Down

0 comments on commit d8017f8

Please sign in to comment.