From 461ef5a4164f96d0db82915365b663e8f01ae201 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Thu, 4 Jun 2026 18:03:06 -0400 Subject: [PATCH 1/2] add linter and update PR template --- AI_GUIDELINES.md | 13 +++++++++++++ Iris/lakefile.toml | 1 + PULL_REQUEST_TEMPLATE.md | 14 ++------------ 3 files changed, 16 insertions(+), 12 deletions(-) create mode 100644 AI_GUIDELINES.md diff --git a/AI_GUIDELINES.md b/AI_GUIDELINES.md new file mode 100644 index 000000000..a790d9d27 --- /dev/null +++ b/AI_GUIDELINES.md @@ -0,0 +1,13 @@ +# Generative AI Guidelines +AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review. +Please carefully review your code to ensure it meets the following standards. + +- Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library. +- `have` statements that do not aid readability or code reuse should be inlined. +- Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line. +- In general, proofs should not perform substantially more case splitting than their Rocq counterparts. + +In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations. +We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work. + + diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml index 2239fdc58..1e74bea0d 100644 --- a/Iris/lakefile.toml +++ b/Iris/lakefile.toml @@ -13,6 +13,7 @@ rev = "v4.30.0" [[lean_lib]] name = "Iris" +lintDriver := "batteries/runLinter" [[lean_lib]] name = "IrisTest" diff --git a/PULL_REQUEST_TEMPLATE.md b/PULL_REQUEST_TEMPLATE.md index 6ae23494e..685779f6b 100644 --- a/PULL_REQUEST_TEMPLATE.md +++ b/PULL_REQUEST_TEMPLATE.md @@ -6,15 +6,5 @@ Fixes # (issue number) ## Checklist * [ ] My code follows the mathlib [naming](https://leanprover-community.github.io/contribute/naming.html) and [code style](https://leanprover-community.github.io/contribute/style.html) conventions * [ ] I have added my name to the `authors` section of any appropriate files - -## Generative AI Guidelines -AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review. -Please carefully review your code to ensure it meets the following standards. - -- Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library. -- `have` statements that do not aid readability or code reuse should be inlined. -- Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line. -- In general, proofs should not perform substantially more case splitting than their Rocq counterparts. - -In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations. -We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work. +* [ ] My code passes the linter (`lake lint`) +* [ ] I have followed the Iris-Lean generative AI guidelines, as outlined in [AI_GUIDELINES.md](https://github.com/leanprover-community/iris-lean/blob/master/AI_GUIDELINES.md) From 19ea45b49beab86e411aa78ba8ccfa1d89d6d388 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Thu, 4 Jun 2026 18:11:27 -0400 Subject: [PATCH 2/2] fix --- Iris/lakefile.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml index 1e74bea0d..6c39df2ac 100644 --- a/Iris/lakefile.toml +++ b/Iris/lakefile.toml @@ -1,5 +1,6 @@ name = "iris" defaultTargets = ["Iris", "IrisTest"] +lintDriver = "batteries/runLinter" [[require]] name = "Qq" @@ -13,7 +14,6 @@ rev = "v4.30.0" [[lean_lib]] name = "Iris" -lintDriver := "batteries/runLinter" [[lean_lib]] name = "IrisTest"