Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cachedMake retrieving incomplete files? #77

Open
Zimmi48 opened this issue Oct 30, 2021 · 2 comments
Open

cachedMake retrieving incomplete files? #77

Zimmi48 opened this issue Oct 30, 2021 · 2 comments

Comments

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 30, 2021

In https://github.com/coq-community/hydra-battles/runs/4054266890?check_suite_focus=true, we got an error of the following form while building a coqdoc target:

/home/runner/work/hydra-battles/hydra-battles/theories/ordinals/Ackermann/wellFormed.vo: premature end of file. Try to rebuild it.

In principle, the file should have been built in a previous job (hydra-battles-single) and retrieved with cachedMake.

Is this possible that this retrieval step led to an incomplete file?

Restarting the job made it pass.

@CohenCyril
Copy link
Collaborator

What does this have to do with cachedMake? I do not see a call to it and it is not used in the toolbox generated CI.

@Zimmi48
Copy link
Member Author

Zimmi48 commented Oct 30, 2021

This build-doc step is manually implemented (and inserted in the generated CI configuration). It does the following:

  build-doc:
    needs:
    - hydra-battles-single
    runs-on: ubuntu-latest
    steps:
    - name: Determine which commit to test
      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{\
        \ github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{\
        \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
        \ | cut -f1)\n  if [ -z \"$merge_commit\" ]; then\n    echo \"tested_commit=${{\
        \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n  else\n    echo\
        \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n  fi\nfi\n"
    - name: Git checkout
      uses: actions/checkout@v2
      with:
        fetch-depth: 0
        ref: ${{ env.tested_commit }}
    - name: Cachix install
      uses: cachix/install-nix-action@v14
      with:
        nix_path: nixpkgs=channel:nixpkgs-unstable
    - name: Cachix setup coq
      uses: cachix/cachix-action@v10
      with:
        name: coq
    - name: Cachix setup coq-community
      uses: cachix/cachix-action@v10
      with:
        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
        name: coq-community
    - name: Cachix setup math-comp
      uses: cachix/cachix-action@v10
      with:
        name: math-comp
    - name: Retrieve prebuilt vo files
      run: |
        nix-shell --run "make Makefile.coq"
        nix-shell --run "cachedMake"
        nix-shell --run "make -t"
    - name: Build Alectryon snippets
      run: nix-shell --run "make -C doc/movies -j $(nproc) all"
    - name: Build coqdoc
      run: nix-shell --run "make -j $(nproc) html"
    - name: Compile LaTeX document
      run: nix-shell --run "make pdf SOURCE_DATE_EPOCH=$(date +%s)"
    - name: Extract PDF and Coqdoc
      run: |
        mkdir -p public/doc public/theories
        cp doc/hydras.pdf public/doc/
        cp -r theories/html public/theories/
    # Depending on whether we are on master or not, we deploy to
    # GitHub Pages or as an artifact
    - name: Deploy to GitHub pages
      if: github.event_name == 'push' && github.ref == 'refs/heads/master'
      uses: crazy-max/ghaction-github-pages@v2
      with:
        build_dir: public
        jekyll: false
      env:
        GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
    - name: Deploy artifact
      if: github.event_name != 'push' || github.ref != 'refs/heads/master'
      uses: actions/upload-artifact@v2
      with:
        path: public

Notice that the step "Retrieve prebuilt vo files" calls cachedMake to retrieve prebuilt vo files.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants