diff options
| -rw-r--r-- | .github/workflows/gh-pages.yml | 29 | ||||
| -rw-r--r-- | README.md | 2 |
2 files changed, 1 insertions, 30 deletions
diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml deleted file mode 100644 index ed7e032..0000000 --- a/.github/workflows/gh-pages.yml +++ /dev/null @@ -1,29 +0,0 @@ -name: docs - -on: - push: - branches: [ master ] - pull_request: - branches: [ master ] - -jobs: - build: - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v2 - - - name: Install emacs - run: sudo apt-get install emacs - - - name: Generate documentation - run: cd docs && emacs --batch --no-init --load publish.el --funcall org-publish-all - - - name: Generate Admitted icon - run: python3 scripts/statistics.py src && mkdir -p docs/html/assets && mv admitted.svg docs/html/assets/. - - - name: Deploy gh-pages - uses: peaceiris/actions-gh-pages@v3 - with: - github_token: ${{ secrets.GITHUB_TOKEN }} - publish_dir: ./docs/html @@ -1,7 +1,7 @@ # Vericert [](https://github.com/ymherklotz/vericert/actions) -[](https://ymherklotz.github.io/vericert) +[](https://vericert.ymhg.org/)  A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [CompCert](https://github.com/AbsInt/CompCert). This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness. |