feat: HasFPowerSeriesAt.eventually_differentiableAt #29
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # DO NOT EDIT THIS FILE!!! | |
| # This file is automatically generated by mk_build_yml.sh | |
| # Edit .github/build.in.yml instead and run | |
| # .github/workflows/mk_build_yml.sh to update. | |
| # Forks of mathlib and other projects should be able to use build_fork.yml directly | |
| # The jobs in this file run on GitHub-hosted workers and will only be run from external forks | |
| on: | |
| push: | |
| branches-ignore: | |
| # ignore tmp branches used by bors | |
| - 'staging.tmp*' | |
| - 'trying.tmp*' | |
| - 'staging*.tmp' | |
| - 'nolints' | |
| name: continuous integration (mathlib forks) | |
| env: | |
| # Disable Lake's automatic fetching of cloud builds. | |
| # Lake's cache is currently incompatible with Mathlib's `lake exe cache`. | |
| # This is because Mathlib's Cache assumes all build artifacts present in the build directory | |
| # are valid by-products of the Mathlib build. Build artifacts fetched from Lake's cache do | |
| # not necessarily satisfy this property. | |
| LAKE_NO_CACHE: true | |
| concurrency: | |
| # label each workflow run; only the latest with each label will run | |
| # workflows on master get more expressive labels | |
| group: ${{ github.workflow }}-${{ github.ref }}. | |
| ${{ ( contains(fromJSON( '["refs/heads/master", "refs/heads/staging"]'), github.ref ) && github.run_id) || ''}} | |
| # cancel any running workflow with the same label | |
| cancel-in-progress: true | |
| jobs: | |
| build: | |
| if: github.repository != 'leanprover-community/mathlib4' | |
| name: Build (fork) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: cleanup | |
| run: | | |
| find . -name . -o -prune -exec rm -rf -- {} + | |
| # Delete all but the 5 most recent toolchains. | |
| # Make sure to delete both the `~/.elan/toolchains/X` directory and the `~/.elan/update-hashes/X` file. | |
| # Skip symbolic links (`-type d`), the current directory (`! -name .`), and `nightly` and `stable`. | |
| if cd ~/.elan/toolchains && find . -maxdepth 1 -type d ! -name . -print0 | xargs -0 ls -1td | grep -v 'nightly$' | grep -v 'stable$' | tail -n +6 | xargs -I {} sh -c 'echo {} && rm -rf "{}" && rm "../update-hashes/{}"'; then | |
| : # Do nothing on success | |
| else | |
| : # Do nothing on failure, but suppress errors | |
| fi | |
| # The Hoskinson runners may not have jq installed, so do that now. | |
| - name: 'Setup jq' | |
| uses: dcarbone/install-jq-action@f0e10f46ff84f4d32178b4b76e1ef180b16f82c3 # v3.1.1 | |
| - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| reinstall-transient-toolchain: true | |
| - name: cleanup .cache/mathlib | |
| run: | | |
| # Define the cache directory path | |
| CACHE_DIR="$HOME/.cache/mathlib" | |
| # Check if directory exists | |
| if [ ! -d "$CACHE_DIR" ]; then | |
| echo "::warning::Cache directory does not exist: $CACHE_DIR" | |
| exit 0 | |
| fi | |
| # Calculate directory size in bytes | |
| DIR_SIZE=$(du -sb "$CACHE_DIR" | cut -f1) | |
| printf 'Cache size (in bytes): %s\n' "$DIR_SIZE" | |
| # Check if size exceeds 10GB | |
| if [ "$DIR_SIZE" -gt "10737418240" ]; then | |
| echo "Cache size exceeds threshold, running lake exe cache clean" | |
| lake exe cache clean || echo "lake did not work" | |
| fi | |
| - name: build cache | |
| run: | | |
| lake build cache | |
| - name: get cache | |
| id: get | |
| run: | | |
| rm -rf .lake/build/lib/lean/Mathlib | |
| # useful pre v4.18: the following command is only present for compatibility reasons | |
| rm -rf .lake/build/lib/Mathlib/ | |
| # Fail quickly if the cache is completely cold, by checking for Mathlib.Init | |
| lake exe cache get Mathlib/Init.lean | |
| lake build --no-build Mathlib.Init && lake exe cache get || echo "No cache for 'Mathlib.Init' available" | |
| - name: update {Mathlib, Tactic, Counterexamples, Archive}.lean | |
| id: mk_all | |
| run: | | |
| if ! lake exe mk_all --check | |
| then | |
| echo "Not all lean files are in the import all files" | |
| echo "mk_all=false" >> "${GITHUB_OUTPUT}" | |
| else | |
| echo "mk_all=true" >> "${GITHUB_OUTPUT}" | |
| fi | |
| - name: build mathlib | |
| id: build | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| linters: lean | |
| run: | | |
| bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI" | |
| - name: print the sizes of the oleans | |
| run: | | |
| du .lake/build/lib/lean/Mathlib || | |
| # This path was the correct path before v4.18: it is here just for compatibility reasons | |
| du .lake/build/lib/Mathlib || echo "This code should be unreachable" | |
| - name: upload cache | |
| # We only upload the cache if the build started (whether succeeding, failing, or cancelled) | |
| # but not if any earlier step failed or was cancelled. | |
| # See discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Some.20files.20not.20found.20in.20the.20cache/near/407183836 | |
| if: ${{ always() && steps.get.outcome == 'success' }} | |
| run: | | |
| # TODO: this is not doing anything currently, and needs to be integrated with put-unpacked | |
| # lake exe cache commit || true | |
| # run this in CI if it gets an incorrect lake hash for existing cache files somehow | |
| # lake exe cache put! | |
| # do not try to upload files just downloaded | |
| lake exe cache put-unpacked | |
| env: | |
| MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} | |
| - name: check the cache | |
| run: | | |
| # Because the `lean-pr-testing-NNNN` branches use toolchains that are "updated in place" | |
| # the cache mechanism is unreliable, so we don't test it if we are on such a branch. | |
| if [[ ! $(cat lean-toolchain) =~ ^leanprover/lean4-pr-releases:pr-release-[0-9]+$ ]]; then | |
| cd DownstreamTest | |
| cp ../lean-toolchain . | |
| MATHLIB_NO_CACHE_ON_UPDATE=1 lake update | |
| lake exe cache get || (sleep 1; lake exe cache get) | |
| # We need to run `lake build ProofWidgets` here to retrieve ProofWidgets via Reservoir. | |
| lake build ProofWidgets | |
| lake build --no-build Mathlib | |
| fi | |
| - name: build archive | |
| id: archive | |
| run: | | |
| # Note: we should not be including `Archive` and `Counterexamples` in the cache. | |
| # We do this for now for the sake of not rebuilding them in every CI run | |
| # even when they are not touched. | |
| # Since `Archive` and `Counterexamples` files have very simple dependencies, | |
| # it should be possible to determine whether they need to be built without actually | |
| # storing and transferring oleans over the network. | |
| # Hopefully a future re-implementation of `cache` will obviate the present need for this hack. | |
| lake exe cache get Archive.lean | |
| bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive" | |
| lake exe cache put Archive.lean | |
| env: | |
| MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} | |
| - name: build counterexamples | |
| id: counterexamples | |
| run: | | |
| lake exe cache get Counterexamples.lean | |
| bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples" | |
| lake exe cache put Counterexamples.lean | |
| env: | |
| MATHLIB_CACHE_SAS: ${{ secrets.MATHLIB_CACHE_SAS }} | |
| MATHLIB_CACHE_S3_TOKEN: ${{ secrets.MATHLIB_CACHE_S3_TOKEN }} | |
| - name: Check {Mathlib, Tactic, Counterexamples, Archive}.lean | |
| run: | | |
| if [ ${{ steps.mk_all.outputs.mk_all }} == "false" ] | |
| then | |
| echo "Please run 'lake exe mk_all' to regenerate the import all files" | |
| exit 1 | |
| fi | |
| - name: check for noisy stdout lines | |
| id: noisy | |
| run: | | |
| buildMsgs="$( | |
| ## we exploit `lake`s replay feature: since the cache is present, running | |
| ## `lake build` will reproduce all the outputs without having to recompute | |
| lake build Mathlib Archive Counterexamples | | |
| ## we filter out the output lines that begin with `✔ [xx/yy]`, where xx, yy | |
| ## are either numbers or ?, and the "Build completed successfully." message. | |
| ## We keep the rest, which are actual outputs of the files | |
| awk '!($0 ~ "^\\s*✔ \\[[?0-9]*/[?0-9]*\\]" || $0 == "Build completed successfully."){ print $0 }')" | |
| if [ -n "${buildMsgs}" ] | |
| then | |
| printf $'%s\n' "${buildMsgs}" | |
| exit 1 | |
| fi | |
| - name: check declarations in db files | |
| run: | | |
| python3 scripts/yaml_check.py docs/100.yaml docs/1000.yaml docs/overview.yaml docs/undergrad.yaml | |
| lake exe check-yaml | |
| - name: generate our import graph | |
| run: lake exe graph | |
| - name: upload the import graph | |
| uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 | |
| with: | |
| name: import-graph | |
| path: import_graph.dot | |
| ## the default is 90, but we build often, so unless there's a reason | |
| ## to care about old copies in the future, just say 7 days for now | |
| retention-days: 7 | |
| - name: clean up the import graph file | |
| run: rm import_graph.dot | |
| - name: build everything | |
| # make sure everything is available for test/import_all.lean | |
| run: | | |
| lake build Batteries Qq Aesop ProofWidgets Plausible | |
| - name: test mathlib | |
| id: test | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| linters: lean | |
| run: | |
| lake --iofail test | |
| - name: check for unused imports | |
| id: shake | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| linters: gcc | |
| run: env LEAN_ABORT_ON_PANIC=1 lake exe shake --gh-style | |
| - name: lint mathlib | |
| if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }} | |
| id: lint | |
| uses: leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23 | |
| with: | |
| linters: gcc | |
| run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter Mathlib | |
| # We no longer run `lean4checker` in regular CI, as it is quite expensive for little benefit. | |
| # Instead we run it in a cron job on master: see `lean4checker.yml`. | |
| # Output is posted to the zulip topic | |
| # https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/lean4checker | |
| - name: Post comments for lean-pr-testing-NNNN and batteries-pr-testing-NNNN branches | |
| if: always() | |
| env: | |
| TOKEN: ${{ secrets.LEAN_PR_TESTING }} | |
| GITHUB_CONTEXT: ${{ toJson(github) }} | |
| WORKFLOW_URL: https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }} | |
| BUILD_OUTCOME: ${{ steps.build.outcome }} | |
| NOISY_OUTCOME: ${{ steps.noisy.outcome }} | |
| ARCHIVE_OUTCOME: ${{ steps.archive.outcome }} | |
| COUNTEREXAMPLES_OUTCOME: ${{ steps.counterexamples.outcome }} | |
| LINT_OUTCOME: ${{ steps.lint.outcome }} | |
| TEST_OUTCOME: ${{ steps.test.outcome }} | |
| run: | | |
| scripts/lean-pr-testing-comments.sh lean | |
| scripts/lean-pr-testing-comments.sh batteries | |
| - name: build lean4checker, but only run it on itself | |
| if: ${{ (always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure') && contains(github.event.pull_request.changed_files, 'lean-toolchain') }} | |
| run: | | |
| git clone https://github.com/leanprover/lean4checker | |
| cd lean4checker | |
| # Read lean-toolchain file and checkout appropriate branch | |
| TOOLCHAIN=$(cat ../lean-toolchain) | |
| if [[ "$TOOLCHAIN" =~ ^leanprover/lean4:v ]]; then | |
| VERSION=${TOOLCHAIN#leanprover/lean4:} | |
| git checkout "$VERSION" | |
| else | |
| git checkout master | |
| fi | |
| # Build lean4checker using the same toolchain | |
| cp ../lean-toolchain . | |
| lake build | |
| lake -q exe lean4checker Lean4Checker | |
| style_lint: | |
| name: Lint style (fork) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: leanprover-community/lint-style-action@f2e7272aad56233a642b08fe974cf09dd664b0c8 # 2025-05-22 | |
| with: | |
| mode: check | |
| lint-bib-file: true | |
| final: | |
| name: Post-CI job (fork) | |
| if: github.repository != 'leanprover-community/mathlib4' | |
| needs: [style_lint, build] | |
| runs-on: ubuntu-latest | |
| steps: | |
| - id: PR | |
| uses: 8BitJonny/gh-get-current-pr@08e737c57a3a4eb24cec6487664b243b77eb5e36 # 3.0.0 | |
| # TODO: this may not work properly if the same commit is pushed to multiple branches: | |
| # https://github.com/8BitJonny/gh-get-current-pr/issues/8 | |
| with: | |
| github-token: ${{ secrets.GITHUB_TOKEN }} | |
| # Only return if PR is still open | |
| filterOutClosed: true | |
| - if: contains(steps.PR.outputs.pr_labels, 'bench-after-CI') | |
| name: If `bench-after-CI` is present, add a `!bench` comment. | |
| uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1 | |
| with: | |
| token: ${{ secrets.AUTO_MERGE_TOKEN }} | |
| issue-number: ${{ steps.PR.outputs.number }} | |
| body: | | |
| !bench | |
| - id: remove_labels | |
| name: Remove "awaiting-CI" | |
| # we use curl rather than octokit/request-action so that the job won't fail | |
| # (and send an annoying email) if the labels don't exist | |
| run: | | |
| curl --request DELETE \ | |
| --url https://api.github.com/repos/${{ github.repository }}/issues/${{ steps.PR.outputs.number }}/labels/awaiting-CI \ | |
| --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | |
| - if: contains(steps.PR.outputs.pr_labels, 'auto-merge-after-CI') | |
| name: If `auto-merge-after-CI` is present, add a `bors merge` comment. | |
| uses: GrantBirki/comment@608e41b19bc973020ec0e189ebfdae935d7fe0cc # v2.1.1 | |
| with: | |
| token: ${{ secrets.AUTO_MERGE_TOKEN }} | |
| issue-number: ${{ steps.PR.outputs.number }} | |
| body: | | |
| As this PR is labelled `auto-merge-after-CI`, we are now sending it to bors: | |
| bors merge |