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

Update documentation in HOL4 examples #1376

Merged
merged 13 commits into from
Dec 20, 2024

Conversation

jhlchan
Copy link
Contributor

@jhlchan jhlchan commented Dec 16, 2024

The examples/algebra library has changed, so the README file is amended.
A paper based on examples/fermat/twosq library is just published, so a reference is added to the README file.

@mn200
Copy link
Member

mn200 commented Dec 16, 2024

You have included automatically generated (but now stale) files under tools/vim and the file tools/hol-mode.el.

@jhlchan
Copy link
Contributor Author

jhlchan commented Dec 16, 2024

I didn't realize that, thanks for pointing them out.

@mn200
Copy link
Member

mn200 commented Dec 17, 2024

You shouldn't git-ignore vim/ ; that causes real files in tools/editor-modes/vim to get ignored.

@mn200
Copy link
Member

mn200 commented Dec 19, 2024

I'm afraid your use of a slash in the middle of an ignore pattern (see output of git help ignore) will not cause old files in tools/vim to be ignored. Given that no-one will ever see these files if they make a fresh checkout, I think it might be cleanest to just not edit .gitignore at all. The effect you're after would be achieved by using the lines

**/vim/file1
**/vim/file2
etc

If you did this, you could then replace the existing .gitignore lines that capture the ignores that are actually present.

@jhlchan
Copy link
Contributor Author

jhlchan commented Dec 19, 2024

I shall leave the modification of .gitignore at your discretion.

@mn200
Copy link
Member

mn200 commented Dec 20, 2024

Thanks for taking the time over this!

@mn200 mn200 merged commit d3fb51b into HOL-Theorem-Prover:develop Dec 20, 2024
4 checks passed
@jhlchan jhlchan deleted the document branch December 20, 2024 02:14
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