diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 1ecc91e22..82fcd026c 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -8,6 +8,15 @@ on: workflow_dispatch: jobs: + cancel: + name: "Cancel Previous Runs" + runs-on: ubuntu-latest + steps: + - uses: styfle/cancel-workflow-action@0.12.1 + with: + all_but_latest: true + access_token: ${{ github.token }} + build: runs-on: ubuntu-latest diff --git a/.github/workflows/check-imports.yml b/.github/workflows/check-imports.yml new file mode 100644 index 000000000..208472c72 --- /dev/null +++ b/.github/workflows/check-imports.yml @@ -0,0 +1,20 @@ +name: Check Imports + +on: + pull_request: + branches: ["main"] + workflow_dispatch: + +jobs: + check-imports: + name: Check Library File Imports + runs-on: ubuntu-latest + steps: + - name: Checkout code + uses: actions/checkout@v4 + + - name: Update Bluebell.lean + run: ./scripts/update-lib.sh + + - name: Check that all files are imported + run: git diff --exit-code src/Bluebell.lean diff --git a/.github/workflows/pr-summary.yml b/.github/workflows/pr-summary.yml new file mode 100644 index 000000000..0827881e6 --- /dev/null +++ b/.github/workflows/pr-summary.yml @@ -0,0 +1,21 @@ +name: 'PR Summary' + +on: + pull_request: + types: [opened, synchronize] + +permissions: + contents: read + pull-requests: write + +jobs: + summarize: + runs-on: ubuntu-latest + steps: + - name: Generate PR Summary + uses: alexanderlhicks/lean-summary-workflow@main + with: + github_token: ${{ secrets.GITHUB_TOKEN }} + gemini_api_key: ${{ secrets.GEMINI_API_KEY }} + github_repository: ${{ github.repository }} + pr_number: ${{ github.event.pull_request.number }} \ No newline at end of file diff --git a/.github/workflows/review.yml b/.github/workflows/review.yml new file mode 100644 index 000000000..6199803de --- /dev/null +++ b/.github/workflows/review.yml @@ -0,0 +1,29 @@ +name: AI Code Review for Lean PRs + +on: + issue_comment: + types: [created] + workflow_dispatch: + inputs: + pr_number: + description: 'Pull Request Number' + required: true + type: string + +jobs: + ai_review_lean: + if: | + (github.event_name == 'issue_comment' && github.event.issue.pull_request && startsWith(github.event.comment.body, '/review') && (github.event.comment.author_association == 'OWNER' || github.event.comment.author_association == 'MEMBER')) || + (github.event_name == 'workflow_dispatch') + runs-on: ubuntu-latest + permissions: + contents: read + pull-requests: write + + steps: + - name: Run AI Code Review Action + uses: alexanderlhicks/lean-review-workflow@main + with: + github_token: ${{ secrets.GITHUB_TOKEN }} + gemini_api_key: ${{ secrets.GEMINI_API_KEY }} + pr_number: ${{ github.event.issue.number || inputs.pr_number }} \ No newline at end of file diff --git a/.github/workflows/sync-upstream.yml b/.github/workflows/sync-upstream.yml new file mode 100644 index 000000000..9a8545d6e --- /dev/null +++ b/.github/workflows/sync-upstream.yml @@ -0,0 +1,150 @@ +name: Sync with Upstream + +on: + schedule: + - cron: "0 9 */14 * *" # Every 14 days at 09:00 AM UTC + workflow_dispatch: # Allow manual triggering + +jobs: + sync_upstream: + runs-on: ubuntu-latest + permissions: + contents: write + pull-requests: write + steps: + - name: Checkout repository + uses: actions/checkout@v4 + with: + token: ${{ secrets.GITHUB_TOKEN }} + fetch-depth: 0 + + - name: Configure Git + run: | + git config --global user.name "github-actions[bot]" + git config --global user.email "github-actions[bot]@users.noreply.github.com" + + - name: Add upstream remote + run: | + git remote add upstream https://github.com/leanprover-community/iris-lean.git || true + git fetch upstream + + - name: Create sync branch + id: sync + run: | + BRANCH_NAME="sync-upstream-$(date +%Y-%m-%d)" + echo "branch_name=$BRANCH_NAME" >> $GITHUB_OUTPUT + + # Check if there are any differences between our master and upstream master + UPSTREAM_COMMITS=$(git rev-list --count HEAD..upstream/master 2>/dev/null || echo "0") + echo "upstream_commits=$UPSTREAM_COMMITS" >> $GITHUB_OUTPUT + + if [ "$UPSTREAM_COMMITS" -eq "0" ]; then + echo "No new commits from upstream. Skipping sync." + echo "needs_sync=false" >> $GITHUB_OUTPUT + exit 0 + fi + + echo "needs_sync=true" >> $GITHUB_OUTPUT + echo "Found $UPSTREAM_COMMITS new commits from upstream" + + # Create and switch to sync branch + git checkout -b "$BRANCH_NAME" + + # Attempt to merge upstream changes + if git merge upstream/master --no-edit; then + echo "merge_success=true" >> $GITHUB_OUTPUT + echo "Upstream changes merged successfully" + else + echo "merge_success=false" >> $GITHUB_OUTPUT + echo "Merge conflicts detected" + # Add all files (including conflicted ones) and commit + git add . + git commit -m "WIP: Sync with upstream - merge conflicts need resolution" + fi + + - name: Push sync branch + if: steps.sync.outputs.needs_sync == 'true' + run: | + git push origin ${{ steps.sync.outputs.branch_name }} + + - name: Create Pull Request + if: steps.sync.outputs.needs_sync == 'true' + uses: actions/github-script@v7 + with: + script: | + const branchName = '${{ steps.sync.outputs.branch_name }}'; + const mergeSuccess = '${{ steps.sync.outputs.merge_success }}' === 'true'; + const upstreamCommits = '${{ steps.sync.outputs.upstream_commits }}'; + + let title, body; + + if (mergeSuccess) { + title = `🔄 Sync with upstream (${upstreamCommits} commits)`; + body = `## Upstream Sync + + This PR automatically syncs changes from \`leanprover-community/iris-lean\`. + + ### Changes + - **${upstreamCommits}** new commits from upstream + - No merge conflicts detected ✅ + + ### Next Steps + - Review the changes + - Run tests to ensure compatibility + - Merge when ready + + --- + *This PR was created automatically by the sync-upstream workflow.*`; + } else { + title = `⚠️ Sync with upstream (${upstreamCommits} commits) - Conflicts Need Resolution`; + body = `## Upstream Sync - Manual Resolution Required + + This PR automatically syncs changes from \`leanprover-community/iris-lean\`, but **merge conflicts were detected** and need manual resolution. + + ### Changes + - **${upstreamCommits}** new commits from upstream + - ⚠️ Merge conflicts detected - manual resolution required + + ### Next Steps + 1. Check out this branch locally: \`git checkout ${branchName}\` + 2. Resolve merge conflicts in the affected files + 3. Commit the resolved changes + 4. Push the updates: \`git push origin ${branchName}\` + 5. Review and merge this PR + + ### Commands to resolve locally: + \`\`\`bash + git checkout ${branchName} + # Resolve conflicts in your editor + git add . + git commit -m "Resolve merge conflicts from upstream sync" + git push origin ${branchName} + \`\`\` + + --- + *This PR was created automatically by the sync-upstream workflow.*`; + } + + const { data: pr } = await github.rest.pulls.create({ + owner: context.repo.owner, + repo: context.repo.repo, + title: title, + head: branchName, + base: 'master', + body: body + }); + + console.log(`Created PR #${pr.number}: ${pr.html_url}`); + + // Add labels based on merge status + const labels = ['upstream-sync']; + if (!mergeSuccess) { + labels.push('merge-conflicts'); + } + + await github.rest.issues.addLabels({ + owner: context.repo.owner, + repo: context.repo.repo, + issue_number: pr.number, + labels: labels + }); \ No newline at end of file diff --git a/.gitignore b/.gitignore index bfb30ec8c..8c01fdc6c 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,19 @@ /.lake +/.claude +/.cursor + +# LaTeX compilation files +*.aux +*.bbl +*.blg +*.fdb_latexmk +*.fls +*.log +*.out +*.synctex.gz +*.synctex(busy) + +# Generated paper PDF +paper/paper.pdf + +.DS_Store.gemini_tmp/ diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 000000000..f8f85cbf3 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,48 @@ +# Contributing to Iris-Lean + +We enthusiastically welcome contributions to this fork of Iris-Lean! + +This project aims to develop the [Bluebell](https://arxiv.org/abs/2402.18708) program logic on top of Iris. Whether you are fixing bugs, improving documentation, or adding new formalizations, your input is valuable. We particularly encourage contributions that address: + +* **Active formalizations:** Please see the [Bluebell paper](https://arxiv.org/abs/2402.18708) for the theoretical foundations and goals of this project. +* **Open Issues:** Please see the list of open issues for bugs, requested features, and specific formalization tasks. Issues tagged as `good first issue` or `help wanted` are great places to start. +* **Documentation:** Documentation is actively being worked on. + +If you are interested in contributing but unsure where to begin, please get in touch via the [Iris-Lean Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean). + +### Large Contributions + +For substantial contributions, such as formalizing a new section of the Bluebell logic, we strongly encourage aligning with the paper first. + +* **Bluebell Paper:** The [Bluebell paper](https://arxiv.org/abs/2402.18708) acts as the primary specification (or "blueprint") for this project. + * It outlines the definitions, theorems, and logical rules we aim to formalize. + * Please verify that your contributions match the definitions and theorems presented in the paper. +* **Process:** Please open a new discussion or issue to propose your planned contribution and discuss how it fits into the existing formalization before starting implementation. + +### Style Guide + +Iris-Lean aims to align closely with the established conventions of the Lean community, particularly those used in `mathlib`. +Please follow the [mathlib Style Guide](https://github.com/leanprover-community/mathlib4/blob/master/CONTRIBUTING.md#style-guide-and-conventions). +This covers naming conventions, proof style, formatting, and more. + +Adhering to this style guide ensures consistency across the library, making it easier for everyone to read, understand, and maintain the code. Please ensure your code compiles and follows these standards. + +#### Citation Standards + +When referencing papers in Lean docstrings: + +* **Use citation keys in text**: Reference papers with citation keys (e.g., `[Bluebell24]`) rather than full titles or URLs. + +* **Include a References section**: Each file that cites papers should have a `## References` section in its docstring header. + +## Code of Conduct + +To ensure a welcoming and collaborative environment, this project follows the principles outlined in the [mathlib Code of Conduct](https://github.com/leanprover-community/mathlib4/blob/master/CODE_OF_CONDUCT.md). + +By participating in this project (e.g., contributing code, opening issues, commenting in discussions), you agree to abide by its terms. Please treat fellow contributors with respect. Unacceptable behavior can be reported to the project maintainers. + +## Licensing + +This project is licensed under the terms of the Apache License 2.0 license. The full license text can be found in the [LICENSE](LICENSE) file. + +By contributing to Iris-Lean, you agree that your contributions will be licensed under this same license. Ensure you are comfortable with these terms before submitting contributions. diff --git a/lake-manifest.json b/lake-manifest.json index 6ac34bfa9..7590fa787 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,15 +1,95 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/quote4", + [{"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bf4cd323a0d088f361a94fcadb8db5cf1e9f3768", - "name": "Qq", + "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", + "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "stable", + "inputRev": "v4.28.0", "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.28.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.28.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.87", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, "configFile": "lakefile.toml"}], "name": "iris", "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index f1c790ac9..dc64ee907 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,14 +1,24 @@ name = "iris" srcDir = "./src/" -defaultTargets = ["Iris", "IrisTest"] +defaultTargets = ["Iris", "Bluebell", "IrisTest"] [[require]] -name = "Qq" +name = "mathlib" scope = "leanprover-community" -version = "git#stable" +rev = "v4.28.0" + +[[require]] +name = "importGraph" +scope = "leanprover-community" +rev = "v4.28.0" [[lean_lib]] name = "Iris" +globs = ["Iris.*"] + +[[lean_lib]] +name = "Bluebell" +globs = ["Bluebell.*"] [[lean_lib]] name = "IrisTest" diff --git a/paper/ACM-Reference-Format.bst b/paper/ACM-Reference-Format.bst new file mode 100644 index 000000000..c47cb4c0f --- /dev/null +++ b/paper/ACM-Reference-Format.bst @@ -0,0 +1,3081 @@ +%%% -*-BibTeX-*- +%%% ==================================================================== +%%% @BibTeX-style-file{ +%%% author = "Nelson H. F. Beebe, Boris Veytsman and Gerald Murray", +%%% version = "2.1", +%%% acmart-version = "1.90", +%%% date = "Mar 26 2023", +%%% filename = "ACM-Reference-Format.bst", +%%% email = "borisv@lk.net, boris@varphi.com", +%%% codetable = "ISO/ASCII", +%%% keywords = "ACM Transactions bibliography style; BibTeX", +%%% license = "public domain", +%%% supported = "yes", +%%% abstract = "", +%%% } +%%% ==================================================================== + +%%% Revision history: see source in git + +ENTRY + { address + advisor + archiveprefix + author + booktitle + chapter + city + date + edition + editor + eprint + eprinttype + eprintclass + howpublished + institution + journal + key + location + month + note + number + organization + pages + primaryclass + publisher + school + series + title + type + volume + year + % New keys recognized + issue % UTAH: used in, e.g., ACM SIGSAM Bulletin and ACM Communications in Computer Algebra + articleno + eid + day % UTAH: needed for newspapers, weeklies, bi-weeklies + doi % UTAH + url % UTAH + bookpages % UTAH + numpages + lastaccessed % UTAH: used only for @Misc{...} + coden % UTAH + isbn % UTAH + isbn-13 % UTAH + issn % UTAH + lccn % UTAH + distinctURL % whether to print url if doi is present + } + {} + { label.year extra.label sort.year sort.label basic.label.year} + +INTEGERS { output.state before.all mid.sentence after.sentence after.block } + +INTEGERS { show-isbn-10-and-13 } % initialized below in begin.bib + +INTEGERS { nameptr namesleft numnames } + +INTEGERS { multiresult } + +INTEGERS { len } + +INTEGERS { last.extra.num } + +STRINGS { s t t.org u } + +STRINGS { last.label next.extra } + +STRINGS { p1 p2 p3 page.count } + + +FUNCTION { not } +{ + { #0 } + { #1 } + if$ +} + +FUNCTION { and } +{ + 'skip$ + { pop$ #0 } + if$ +} + +FUNCTION { or } +{ + { pop$ #1 } + 'skip$ + if$ +} + + +FUNCTION { dump.stack.1 } +{ + duplicate$ "STACK[top] = [" swap$ * "]" * warning$ +} + +FUNCTION { dump.stack.2 } +{ + duplicate$ "STACK[top ] = [" swap$ * "]" * warning$ + swap$ + duplicate$ "STACK[top-1] = [" swap$ * "]" * warning$ + swap$ +} + +FUNCTION { empty.or.unknown } +{ + %% Examine the top stack entry, and push 1 if it is empty, or + %% consists only of whitespace, or is a string beginning with two + %% queries (??), and otherwise, push 0. + %% + %% This function provides a replacement for empty$, with the + %% convenient feature that unknown values marked by two leading + %% queries are treated the same as missing values, and thus, do not + %% appear in the output .bbl file, and yet, their presence in .bib + %% file(s) serves to mark values which are temporarily missing, but + %% are expected to be filled in eventually once more data is + %% obtained. The TeX User Group and BibNet bibliography archives + %% make extensive use of this practice. + %% + %% An empty string cannot serve the same purpose, because just as in + %% statistics data processing, an unknown value is not the same as an + %% empty value. + %% + %% At entry: stack = ... top:[string] + %% At exit: stack = ... top:[0 or 1] + + duplicate$ empty$ + { pop$ #1 } + { #1 #2 substring$ "??" = } + if$ +} + +FUNCTION { empty.or.zero } +{ + %% Examine the top entry and push 1 if it is empty, or is zero + duplicate$ empty$ + { pop$ #1 } + { "0" = } + if$ +} + + +FUNCTION { writeln } +{ + %% In BibTeX style files, the sequences + %% + %% ... "one" "two" output + %% ... "one" "two" output.xxx + %% + %% ship "one" to the output file, possibly following by punctuation, + %% leaving the stack with + %% + %% ... "two" + %% + %% There is thus a one-string lag in output processing that must be + %% carefully handled to avoid duplicating a string in the output + %% file. Unless otherwise noted, all output.xxx functions leave + %% just one new string on the stack, and that model should be born + %% in mind when reading or writing function code. + %% + %% BibTeX's asynchronous buffering of output from strings from the + %% stack is confusing because newline$ bypasses the buffer. It + %% would have been so much easier for newline to be a character + %% rather than a state of the output-in-progress. + %% + %% The documentation in btxhak.dvi is WRONG: it says + %% + %% newline$ Writes onto the bbl file what's accumulated in the + %% output buffer. It writes a blank line if and only + %% if the output buffer is empty. Since write$ does + %% reasonable line breaking, you should use this + %% function only when you want a blank line or an + %% explicit line break. + %% + %% write$ Pops the top (string) literal and writes it on the + %% output buffer (which will result in stuff being + %% written onto the bbl file when the buffer fills + %% up). + %% + %% Examination of the BibTeX source code shows that write$ does + %% indeed behave as claimed, but newline$ sends a newline character + %% directly to the output file, leaving the stack unchanged. The + %% first line "Writes onto ... buffer." is therefore wrong. + %% + %% The original BibTeX style files almost always use "write$ newline$" + %% in that order, so it makes sense to hide that pair in a private + %% function like this one, named after a statement in Pascal, + %% the programming language embedded in the BibTeX Web program. + + write$ % output top-of-stack string + newline$ % immediate write of newline (not via stack) +} + +FUNCTION { init.state.consts } +{ + #0 'before.all := + #1 'mid.sentence := + #2 'after.sentence := + #3 'after.block := +} + +FUNCTION { output.nonnull } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = + { + ", " * write$ + } + { + output.state after.block = + { + add.period$ writeln + "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output.nonnull.dot.space } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = % { ". " * write$ } + { + ". " * write$ + } + { + output.state after.block = + { + add.period$ writeln "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output.nonnull.remove } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = + { + " " * write$ + } + { + output.state after.block = + { + add.period$ writeln "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output.nonnull.removenospace } +{ % Stack in: ... R S T Stack out: ... R T File out: S + 's := + output.state mid.sentence = + { + "" * write$ + } + { + output.state after.block = + { + add.period$ writeln "\newblock " write$ + } + { + output.state before.all = + { + write$ + } + { + add.period$ " " * write$ + } + if$ + } + if$ + mid.sentence 'output.state := + } + if$ + s +} + +FUNCTION { output } +{ % discard top token if empty, else like output.nonnull + duplicate$ empty.or.unknown + 'pop$ + 'output.nonnull + if$ +} + +FUNCTION { output.dot.space } +{ % discard top token if empty, else like output.nonnull.dot.space + duplicate$ empty.or.unknown + 'pop$ + 'output.nonnull.dot.space + if$ +} + +FUNCTION { output.removenospace } +{ % discard top token if empty, else like output.nonnull.removenospace + duplicate$ empty.or.unknown + 'pop$ + 'output.nonnull.removenospace + if$ +} + +FUNCTION { output.check } +{ % like output, but warn if key name on top-of-stack is not set + 't := + duplicate$ empty.or.unknown + { pop$ "empty " t * " in " * cite$ * warning$ } + 'output.nonnull + if$ +} + +FUNCTION { bibinfo.output.check } +{ % like output.check, adding bibinfo field + 't := + duplicate$ empty.or.unknown + { pop$ "empty " t * " in " * cite$ * warning$ } + { "\bibinfo{" t "}{" * * swap$ * "}" * + output.nonnull } + if$ +} + +FUNCTION { output.check.dot.space } +{ % like output.dot.space, but warn if key name on top-of-stack is not set + 't := + duplicate$ empty.or.unknown + { pop$ "empty " t * " in " * cite$ * warning$ } + 'output.nonnull.dot.space + if$ +} + +FUNCTION { fin.block } +{ % functionally, but not logically, identical to fin.entry + add.period$ + writeln +} + +FUNCTION { fin.entry } +{ + add.period$ + writeln +} + +FUNCTION { new.sentence } +{ % update sentence state, with neither output nor stack change + output.state after.block = + 'skip$ + { + output.state before.all = + 'skip$ + { after.sentence 'output.state := } + if$ + } + if$ +} + +FUNCTION { fin.sentence } +{ + add.period$ + write$ + new.sentence + "" +} + +FUNCTION { new.block } +{ + output.state before.all = + 'skip$ + { after.block 'output.state := } + if$ +} + +FUNCTION { output.coden } % UTAH +{ % output non-empty CODEN as one-line sentence (stack untouched) + coden empty.or.unknown + { } + { "\showCODEN{" coden * "}" * writeln } + if$ +} + +% +% Sometimes articleno starts with the word 'Article' or 'Paper. +% (this is a bug of acmdl, sigh) +% We strip them. We assume eid or articleno is already on stack +% + +FUNCTION { strip.articleno.or.eid } +{ + 't := + t #1 #7 substring$ "Article" = + {t #8 t text.length$ substring$ 't :=} + { } + if$ + t #1 #7 substring$ "article" = + {t #8 t text.length$ substring$ 't :=} + { } + if$ + t #1 #5 substring$ "Paper" = + {t #6 t text.length$ substring$ 't :=} + { } + if$ + t #1 #5 substring$ "paper" = + {t #6 t text.length$ substring$ 't :=} + { } + if$ + % Strip any left trailing space or ~ + t #1 #1 substring$ " " = + {t #2 t text.length$ substring$ 't :=} + { } + if$ + t #1 #1 substring$ "~" = + {t #2 t text.length$ substring$ 't :=} + { } + if$ + t +} + + +FUNCTION { format.articleno } +{ + articleno empty.or.unknown not eid empty.or.unknown not and + { "Both articleno and eid are defined for " cite$ * warning$ } + 'skip$ + if$ + articleno empty.or.unknown eid empty.or.unknown and + { "" } + { + numpages empty.or.unknown + { "articleno or eid field, but no numpages field, in " + cite$ * warning$ } + { } + if$ + eid empty.or.unknown + { "Article \bibinfo{articleno}{" articleno strip.articleno.or.eid * "}" * } + { "Article \bibinfo{articleno}{" eid strip.articleno.or.eid * "}" * } + if$ + } + if$ +} + +FUNCTION { format.year } +{ % push year string or "[n.\,d.]" onto output stack + %% Because year is a mandatory field, we always force SOMETHING + %% to be output + "\bibinfo{year}{" + year empty.or.unknown + { "[n.\,d.]" } + { year } + if$ + * "}" * +} + +FUNCTION { format.day.month } +{ % push "day month " or "month " or "" onto output stack + day empty.or.unknown + { + month empty.or.unknown + { "" } + { "\bibinfo{date}{" month * "} " *} + if$ + } + { + month empty.or.unknown + { "" } + { "\bibinfo{date}{" day * " " * month * "} " *} + if$ + } + if$ +} + +FUNCTION { format.day.month.year } % UTAH +{ % if month is empty, push "" else push "(MON.)" or "(DD MON.)" + % Needed for frequent periodicals: 2008. ... New York Times C-1, C-2, C-17 (23 Oct.) + % acm-*.bst addition: prefix parenthesized date string with + % ", Article nnn " + articleno empty.or.unknown eid empty.or.unknown and + { "" } + { output.state after.block = + {", " format.articleno * } + { format.articleno } + if$ + } + if$ + " (" * format.day.month * format.year * ")" * +} + +FUNCTION { output.day.month.year } % UTAH +{ % if month is empty value, do nothing; else output stack top and + % leave with new top string "(MON.)" or "(DD MON.)" + % Needed for frequent periodicals: 2008. ... New York Times C-1, C-2, C-17 (23 Oct.) + format.day.month.year + output.nonnull.remove +} + +FUNCTION { strip.doi } % UTAH +{ % Strip any Web address prefix to recover the bare DOI, leaving the + % result on the output stack, as recommended by CrossRef DOI + % documentation. + % For example, reduce "http://doi.acm.org/10.1145/1534530.1534545" to + % "10.1145/1534530.1534545". A suitable URL is later typeset and + % displayed as the LAST item in the reference list entry. Publisher Web + % sites wrap this with a suitable link to a real URL to resolve the DOI, + % and the master https://doi.org/ address is preferred, since publisher- + % specific URLs can disappear in response to economic events. All + % journals are encouraged by the DOI authorities to use that typeset + % format and link procedures for uniformity across all publications that + % include DOIs in reference lists. + % The numeric prefix is guaranteed to start with "10.", so we use + % that as a test. + % 2017-02-04 Added stripping of https:// (Boris) + doi #1 #3 substring$ "10." = + { doi } + { + doi 't := % get modifiable copy of DOI + + % Change https:// to http:// to strip both prefixes (BV) + + t #1 #8 substring$ "https://" = + { "http://" t #9 t text.length$ #8 - substring$ * 't := } + { } + if$ + + t #1 #7 substring$ "http://" = + { + t #8 t text.length$ #7 - substring$ 't := + + "INTERNAL STYLE-FILE ERROR" 's := + + % search for next "/" and assign its suffix to s + + { t text.length$ } + { + t #1 #1 substring$ "/" = + { + % save rest of string as true DOI (should be 10.xxxx/yyyy) + t #2 t text.length$ #1 - substring$ 's := + "" 't := % empty string t terminates the loop + } + { + % discard first character and continue loop: t <= substring(t,2,last) + t #2 t text.length$ #1 - substring$ 't := + } + if$ + } + while$ + + % check for valid DOI (should be 10.xxxx/yyyy) + s #1 #3 substring$ "10." = + { } + { "unrecognized DOI substring " s * " in DOI value [" * doi * "]" * warning$ } + if$ + + s % push the stripped DOI on the output stack + + } + { + "unrecognized DOI value [" doi * "]" * warning$ + doi % push the unrecognized original DOI on the output stack + } + if$ + } + if$ +} + +% +% Change by BV: added standard prefix to URL +% +FUNCTION { output.doi } % UTAH +{ % output non-empty DOI as one-line sentence (stack untouched) + doi empty.or.unknown + { } + { + %% Use \urldef here for the same reason it is used in output.url, + %% see output.url for further discussion. + "\urldef\tempurl%" writeln + "\url{https://doi.org/" strip.doi * "}" * writeln + "\showDOI{\tempurl}" writeln + } + if$ +} + +FUNCTION { output.isbn } % UTAH +{ % output non-empty ISBN-10 and/or ISBN-13 as one-line sentences (stack untouched) + show-isbn-10-and-13 + { + %% show both 10- and 13-digit ISBNs + isbn empty.or.unknown + { } + { + "\showISBNx{" isbn * "}" * writeln + } + if$ + isbn-13 empty.or.unknown + { } + { + "\showISBNxiii{" isbn-13 * "}" * writeln + } + if$ + } + { + %% show 10-digit ISBNs only if 13-digit ISBNs not available + isbn-13 empty.or.unknown + { + isbn empty.or.unknown + { } + { + "\showISBNx{" isbn * "}" * writeln + } + if$ + } + { + "\showISBNxiii{" isbn-13 * "}" * writeln + } + if$ + } + if$ +} + +FUNCTION { output.issn } % UTAH +{ % output non-empty ISSN as one-line sentence (stack untouched) + issn empty.or.unknown + { } + { "\showISSN{" issn * "}" * writeln } + if$ +} + +FUNCTION { output.issue } +{ % output non-empty issue number as a one-line sentence (stack untouched) + issue empty.or.unknown + { } + { "Issue " issue * "." * writeln } + if$ +} + +FUNCTION { output.lccn } % UTAH +{ % return with stack untouched + lccn empty.or.unknown + { } + { "\showLCCN{" lccn * "}" * writeln } + if$ +} + +FUNCTION { output.note } % UTAH +{ % return with stack empty + note empty.or.unknown + { } + { "\shownote{" note * "}" add.period$ * writeln } + if$ +} + +FUNCTION { output.note.check } % UTAH +{ % return with stack empty + note empty.or.unknown + { "empty note in " cite$ * warning$ } + { "\shownote{" note * "}" add.period$ * writeln } + if$ +} + +FUNCTION { output.eprint } % +{ % return with stack empty + eprint empty.or.unknown + { } + { "\showeprint" + archiveprefix empty.or.unknown + { eprinttype empty.or.unknown + { } + { "[" eprinttype "]" * * * } + if$ + } + { "[" archiveprefix "l" change.case$ "]" * * * } + if$ + "{" eprint "}" * * * + primaryclass empty.or.unknown + { eprintclass empty.or.unknown + { } + { "~[" eprintclass "]" * * * } + if$ + } + { "~[" primaryclass "]" * * * } + if$ + writeln + } + if$ +} + + +% +% Changes by BV 2011/04/15. Do not output +% url if doi is defined +% +% +% Changes by BV 2021/11/26. Output url even if doi is defined +% if distinctURL is not zero. +% +FUNCTION { output.url } % UTAH +{ % return with stack untouched + % output URL and associated lastaccessed fields + doi empty.or.unknown distinctURL empty.or.zero not or + { + url empty.or.unknown + { } + { + %% Use \urldef, outside \showURL, so that %nn, #, etc in URLs work + %% correctly. Put the actual URL on its own line to reduce the + %% likelihood of BibTeX's nasty line wrapping after column 79. + %% \url{} can undo this, but if that doesn't work for some reason + %% the .bbl file would have to be repaired manually. + "\urldef\tempurl%" writeln + "\url{" url * "}" * writeln + + "\showURL{%" writeln + lastaccessed empty.or.unknown + { "" } + { "Retrieved " lastaccessed * " from " * } + if$ + "\tempurl}" * writeln + } + if$ + } + { } + if$ +} + +FUNCTION { output.year.check } +{ % warn if year empty, output top string and leave " YEAR