CI

Stream: condensed mathematics

[Eric Wieser]

No, github artifacts are always zips (although I think changing this is on their roadmap)

[Eric Wieser]

If there's an associated gh-pages repo, you could deploy the PDF there

[Eric Wieser]

Like what doc-gen does

[Adam Topaz]

I don't think this is true. Here's the (bad) CI script I had for my class last term:

name: Make Release
on:
  schedule:
    - cron: '0 0 1 1 *'
  workflow_dispatch:
jobs:
  build:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v2
      - name: Compile pdf
        run: |
          sudo apt-get install texlive texlive-latex-recommended texlive-latex-extra --no-install-recommends -qq > /dev/null
          sudo apt-get install texlive-bibtex-extra texlive-pictures latexmk --no-install-recommends -qq > /dev/null
          latexmk --pdf main.tex
      - name: Get current date
        id: date
        run: echo "date=$(date +'%Y-%m-%d')" >> $GITHUB_ENV
      - name: Create Release
        id: create_release
        uses: actions/create-release@v1
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          tag_name: ${{ env.date }}
          release_name: ${{ env.date }}
          #tag_name: ${{ github.run_id }}
          #release_name: ${{ github.sha }}
          body: |
            Release
          draft: false
          prerelease: false
      - name: Upload Release Asset
        id: upload-release-asset
        uses: actions/upload-release-asset@v1
        env:
          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        with:
          upload_url: ${{ steps.create_release.outputs.upload_url }}
          asset_path: ./main.pdf
          asset_name: main.pdf
          asset_content_type: application/pdf

[Adam Topaz]

This builds a PDF and adds it as a file in the release

[Adam Topaz]

Oh, as an artifact maybe it can only be a zip, but you can certainly make a PDF be part of a release

[Bryan Gin-ge Chen]

The CI script creates GitHub releases (with the PDF) as well; the problem is that you have to explicitly tag the commits with git to create a release.

[Adam Topaz]

Ah, I see.

[Riccardo Brasca]

Can someone that understand CI have a quick look at the error we have? The linter says

/home/runner/work/lean-liquid/lean-liquid/scripts/lint_project.lean:9:0: error: invalid import: for_mathlib.derived.K
could not resolve import: for_mathlib.derived.K
<unknown>:1:1: error: could not resolve import: for_mathlib.derived.K
Error: Process completed with exit code 1.

This file does not exist, but I don't know why it is looking for it.

[Adam Topaz]

It's possible that the hyphen in K-projective.lean is an issue. I'll rename it to K_projective

[Adam Topaz]

Okay, I pushed the rename. Let's hope that works!

[Alex J. Best]

If you want hyphens in names you have to wrap them in french quotes for many things, so its best not to use them :smile:

[Eric Rodriguez]

#11001, for a mathlib issue tracking the same thing

[Riccardo Brasca]

It worked, thanks! (The errors we have now are different ones)