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

Adapt to https://github.com/coq/coq/pull/19530 #15

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

proux01
Copy link

@proux01 proux01 commented Sep 17, 2024

Adapt to coq/coq#19530
This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the future).
Merging this is not required for the upstream PR, you can do whatever you want with it.

@proux01 proux01 mentioned this pull request Sep 17, 2024
43 tasks
@liyishuai
Copy link
Collaborator

As mentioned in #10 (comment), changes to the textbook first get merged into a private source repo, and then compiles to here.

Please acknowledge the following copyright transfer, and send an email to @bcpierce00.

sf/lf-current/Preface.v

Lines 452 to 491 in 43b800e

(* ################################################################# *)
(** * Note for Instructors and Contributors *)
(** If you plan to use these materials in your own teaching, or if you
are using software foundations for self study and are finding
things you'd like to help add or improve, your contributions are
welcome! You are warmly invited to join the private SF git repo.
In order to keep the legalities simple and to have a single point
of responsibility in case the need should ever arise to adjust the
license terms, sublicense, etc., we ask all contributors (i.e.,
everyone with access to the developers' repository) to assign
copyright in their contributions to the appropriate "author of
record," as follows:
- I hereby assign copyright in my past and future contributions
to the Software Foundations project to the Author of Record of
each volume or component, to be licensed under the same terms
as the rest of Software Foundations. I understand that, at
present, the Authors of Record are as follows: For Volumes 1
and 2, known until 2016 as "Software Foundations" and from
2016 as (respectively) "Logical Foundations" and "Programming
Foundations," and for Volume 4, "QuickChick: Property-Based
Testing in Coq," the Author of Record is Benjamin C. Pierce.
For Volume 3, "Verified Functional Algorithms," and volume 5,
"Verifiable C," the Author of Record is Andrew W. Appel. For
Volume 6, "Separation Logic Foundations," the author of record
is Arthur Chargueraud. For components outside of designated
volumes (e.g., typesetting and grading tools and other
software infrastructure), the Author of Record is Benjamin
Pierce.
To get started, please send an email to Benjamin Pierce,
describing yourself and how you plan to use the materials and
including (1) the above copyright transfer text and (2) your
github username.
We'll set you up with access to the git repository and developers'
mailing lists. In the repository you'll find the files
[INSTRUCTORS] and [CONTRIBUTING] with further instructions. *)

@proux01
Copy link
Author

proux01 commented Sep 23, 2024

@liyishuai the policy of Coq CI is that the repo/branch in there should accept overlay PRs. Do you confirm that such PRs should instead go to another repo (which one?), in that case, we should at the very least mention this in https://github.com/coq/coq/blob/718eabc3e8a6ad877ca875fa6647b931b5ffadd4/dev/ci/ci-basic-overlay.sh#L456-L457

@liyishuai
Copy link
Collaborator

Yes, this repo is a compilation result, rather than a "source code".

@bcpierce00 Do you feel like handling this PR and editing the documentation for Coq CI?

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