Skip to content

lib/monads: use experiment for demo lemmas #139

lib/monads: use experiment for demo lemmas

lib/monads: use experiment for demo lemmas #139

Workflow file for this run

# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: BSD-2-Clause
# Theory Linter action
name: Lint
# needs pull_request_target trigger for more authority on GITHUB_TOKEN when PR
# originates on a fork
on: [pull_request_target]
jobs:
thylint:
name: 'Theory Linter'
runs-on: ubuntu-latest
steps:
- uses: seL4/ci-actions/thylint@master
with:
token: ${{ secrets.READ_TOKEN }}
pr_num: ${{ github.event.pull_request.number }}
- uses: yuzutech/[email protected]
with:
repo-token: "${{ secrets.GITHUB_TOKEN }}"
title: 'File annotations for theory linter'
input: './annotations.json'
continue-on-error: true
if: always()