Skip to content

feat: create Lean.gitignore#4828

Open
quantum9Innovation wants to merge 1 commit intogithub:mainfrom
quantum9Innovation:lean-gitignore
Open

feat: create Lean.gitignore#4828
quantum9Innovation wants to merge 1 commit intogithub:mainfrom
quantum9Innovation:lean-gitignore

Conversation

@quantum9Innovation
Copy link
Copy Markdown
Contributor

Reasons for making this change

This adds a standard gitignore template for the Lean programming language.

Links to documentation supporting these rule changes

This page describes how Lake, Lean's package manager, works. Currently the template only ignores .lake which is where cache and other data is stored. Others are welcome to add/suggest other useful things to add to the gitignore template, though most Lean projects typically only have this in their gitignore.

If this is a new template

Lean project homepage: https://lean-lang.org/

Merge and Approval Steps

  • Confirm that you've read the contribution guidelines and ensured your PR aligns
  • Ensure CI is passing
  • Get a review and Approval from one of the maintainers

@quantum9Innovation quantum9Innovation requested a review from a team as a code owner March 29, 2026 04:47
Copilot AI review requested due to automatic review settings March 29, 2026 04:47
Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Adds a new .gitignore template for Lean projects to ignore Lake build artifacts, aligning with how Lean’s Lake tool stores cache/build data.

Changes:

  • Introduce Lean.gitignore with rules to ignore Lake’s .lake directory.
  • Add a brief header comment describing the ignored path.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

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

Successfully merging this pull request may close these issues.

2 participants