Skip to content

Commit 09aeed1

Browse files
Add non-commercial license, TODO next steps in README and docs
1 parent 6bc457d commit 09aeed1

3 files changed

Lines changed: 67 additions & 191 deletions

File tree

LICENSE

Lines changed: 36 additions & 190 deletions
Original file line numberDiff line numberDiff line change
@@ -1,202 +1,48 @@
1+
MIT License + Commons Clause
12

2-
Apache License
3-
Version 2.0, January 2004
4-
http://www.apache.org/licenses/
3+
Copyright (c) 2025 Kernel Science (https://kernel-science.com)
54

6-
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
5+
---
76

8-
1. Definitions.
7+
Commons Clause License Condition v1.0
98

10-
"License" shall mean the terms and conditions for use, reproduction,
11-
and distribution as defined by Sections 1 through 9 of this document.
9+
The Software is provided to you by the Licensor under the License, as defined
10+
below, subject to the following condition.
1211

13-
"Licensor" shall mean the copyright owner or entity authorized by
14-
the copyright owner that is granting the License.
12+
Without limiting other conditions in the License, the grant of rights under the
13+
License will not include, and the License does not grant to you, the right to
14+
Sell the Software.
1515

16-
"Legal Entity" shall mean the union of the acting entity and all
17-
other entities that control, are controlled by, or are under common
18-
control with that entity. For the purposes of this definition,
19-
"control" means (i) the power, direct or indirect, to cause the
20-
direction or management of such entity, whether by contract or
21-
otherwise, or (ii) ownership of fifty percent (50%) or more of the
22-
outstanding shares, or (iii) beneficial ownership of such entity.
16+
For purposes of the foregoing, "Sell" means practicing any or all of the rights
17+
granted to you under the License to provide to third parties, for a fee or other
18+
consideration (including without limitation fees for hosting or
19+
consulting/support services related to the Software), a product or service whose
20+
value derives, entirely or substantially, from the functionality of the Software.
21+
Any license notice or attribution required by the License must also include this
22+
Commons Clause License Condition notice.
2323

24-
"You" (or "Your") shall mean an individual or Legal Entity
25-
exercising permissions granted by this License.
24+
Software: PhyslibSearch
25+
License: MIT License
26+
Licensor: Kernel Science (https://kernel-science.com)
2627

27-
"Source" form shall mean the preferred form for making modifications,
28-
including but not limited to software source code, documentation
29-
source, and configuration files.
28+
---
3029

31-
"Object" form shall mean any form resulting from mechanical
32-
transformation or translation of a Source form, including but
33-
not limited to compiled object code, generated documentation,
34-
and conversions to other media types.
30+
MIT License
3531

36-
"Work" shall mean the work of authorship, whether in Source or
37-
Object form, made available under the License, as indicated by a
38-
copyright notice that is included in or attached to the work
39-
(an example is provided in the Appendix below).
32+
Permission is hereby granted, free of charge, to any person obtaining a copy of
33+
this software and associated documentation files (the "Software"), to deal in
34+
the Software without restriction, including without limitation the rights to use,
35+
copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the
36+
Software, and to permit persons to whom the Software is furnished to do so,
37+
subject to the following conditions:
4038

41-
"Derivative Works" shall mean any work, whether in Source or Object
42-
form, that is based on (or derived from) the Work and for which the
43-
editorial revisions, annotations, elaborations, or other modifications
44-
represent, as a whole, an original work of authorship. For the purposes
45-
of this License, Derivative Works shall not include works that remain
46-
separable from, or merely link (or bind by name) to the interfaces of,
47-
the Work and Derivative Works thereof.
39+
The above copyright notice, this permission notice, and the Commons Clause
40+
License Condition above shall be included in all copies or substantial portions
41+
of the Software.
4842

49-
"Contribution" shall mean any work of authorship, including
50-
the original version of the Work and any modifications or additions
51-
to that Work or Derivative Works thereof, that is intentionally
52-
submitted to Licensor for inclusion in the Work by the copyright owner
53-
or by an individual or Legal Entity authorized to submit on behalf of
54-
the copyright owner. For the purposes of this definition, "submitted"
55-
means any form of electronic, verbal, or written communication sent
56-
to the Licensor or its representatives, including but not limited to
57-
communication on electronic mailing lists, source code control systems,
58-
and issue tracking systems that are managed by, or on behalf of, the
59-
Licensor for the purpose of discussing and improving the Work, but
60-
excluding communication that is conspicuously marked or otherwise
61-
designated in writing by the copyright owner as "Not a Contribution."
62-
63-
"Contributor" shall mean Licensor and any individual or Legal Entity
64-
on behalf of whom a Contribution has been received by Licensor and
65-
subsequently incorporated within the Work.
66-
67-
2. Grant of Copyright License. Subject to the terms and conditions of
68-
this License, each Contributor hereby grants to You a perpetual,
69-
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
70-
copyright license to reproduce, prepare Derivative Works of,
71-
publicly display, publicly perform, sublicense, and distribute the
72-
Work and such Derivative Works in Source or Object form.
73-
74-
3. Grant of Patent License. Subject to the terms and conditions of
75-
this License, each Contributor hereby grants to You a perpetual,
76-
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
77-
(except as stated in this section) patent license to make, have made,
78-
use, offer to sell, sell, import, and otherwise transfer the Work,
79-
where such license applies only to those patent claims licensable
80-
by such Contributor that are necessarily infringed by their
81-
Contribution(s) alone or by combination of their Contribution(s)
82-
with the Work to which such Contribution(s) was submitted. If You
83-
institute patent litigation against any entity (including a
84-
cross-claim or counterclaim in a lawsuit) alleging that the Work
85-
or a Contribution incorporated within the Work constitutes direct
86-
or contributory patent infringement, then any patent licenses
87-
granted to You under this License for that Work shall terminate
88-
as of the date such litigation is filed.
89-
90-
4. Redistribution. You may reproduce and distribute copies of the
91-
Work or Derivative Works thereof in any medium, with or without
92-
modifications, and in Source or Object form, provided that You
93-
meet the following conditions:
94-
95-
(a) You must give any other recipients of the Work or
96-
Derivative Works a copy of this License; and
97-
98-
(b) You must cause any modified files to carry prominent notices
99-
stating that You changed the files; and
100-
101-
(c) You must retain, in the Source form of any Derivative Works
102-
that You distribute, all copyright, patent, trademark, and
103-
attribution notices from the Source form of the Work,
104-
excluding those notices that do not pertain to any part of
105-
the Derivative Works; and
106-
107-
(d) If the Work includes a "NOTICE" text file as part of its
108-
distribution, then any Derivative Works that You distribute must
109-
include a readable copy of the attribution notices contained
110-
within such NOTICE file, excluding those notices that do not
111-
pertain to any part of the Derivative Works, in at least one
112-
of the following places: within a NOTICE text file distributed
113-
as part of the Derivative Works; within the Source form or
114-
documentation, if provided along with the Derivative Works; or,
115-
within a display generated by the Derivative Works, if and
116-
wherever such third-party notices normally appear. The contents
117-
of the NOTICE file are for informational purposes only and
118-
do not modify the License. You may add Your own attribution
119-
notices within Derivative Works that You distribute, alongside
120-
or as an addendum to the NOTICE text from the Work, provided
121-
that such additional attribution notices cannot be construed
122-
as modifying the License.
123-
124-
You may add Your own copyright statement to Your modifications and
125-
may provide additional or different license terms and conditions
126-
for use, reproduction, or distribution of Your modifications, or
127-
for any such Derivative Works as a whole, provided Your use,
128-
reproduction, and distribution of the Work otherwise complies with
129-
the conditions stated in this License.
130-
131-
5. Submission of Contributions. Unless You explicitly state otherwise,
132-
any Contribution intentionally submitted for inclusion in the Work
133-
by You to the Licensor shall be under the terms and conditions of
134-
this License, without any additional terms or conditions.
135-
Notwithstanding the above, nothing herein shall supersede or modify
136-
the terms of any separate license agreement you may have executed
137-
with Licensor regarding such Contributions.
138-
139-
6. Trademarks. This License does not grant permission to use the trade
140-
names, trademarks, service marks, or product names of the Licensor,
141-
except as required for reasonable and customary use in describing the
142-
origin of the Work and reproducing the content of the NOTICE file.
143-
144-
7. Disclaimer of Warranty. Unless required by applicable law or
145-
agreed to in writing, Licensor provides the Work (and each
146-
Contributor provides its Contributions) on an "AS IS" BASIS,
147-
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
148-
implied, including, without limitation, any warranties or conditions
149-
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
150-
PARTICULAR PURPOSE. You are solely responsible for determining the
151-
appropriateness of using or redistributing the Work and assume any
152-
risks associated with Your exercise of permissions under this License.
153-
154-
8. Limitation of Liability. In no event and under no legal theory,
155-
whether in tort (including negligence), contract, or otherwise,
156-
unless required by applicable law (such as deliberate and grossly
157-
negligent acts) or agreed to in writing, shall any Contributor be
158-
liable to You for damages, including any direct, indirect, special,
159-
incidental, or consequential damages of any character arising as a
160-
result of this License or out of the use or inability to use the
161-
Work (including but not limited to damages for loss of goodwill,
162-
work stoppage, computer failure or malfunction, or any and all
163-
other commercial damages or losses), even if such Contributor
164-
has been advised of the possibility of such damages.
165-
166-
9. Accepting Warranty or Additional Liability. While redistributing
167-
the Work or Derivative Works thereof, You may choose to offer,
168-
and charge a fee for, acceptance of support, warranty, indemnity,
169-
or other liability obligations and/or rights consistent with this
170-
License. However, in accepting such obligations, You may act only
171-
on Your own behalf and on Your sole responsibility, not on behalf
172-
of any other Contributor, and only if You agree to indemnify,
173-
defend, and hold each Contributor harmless for any liability
174-
incurred by, or claims asserted against, such Contributor by reason
175-
of your accepting any such warranty or additional liability.
176-
177-
END OF TERMS AND CONDITIONS
178-
179-
APPENDIX: How to apply the Apache License to your work.
180-
181-
To apply the Apache License to your work, attach the following
182-
boilerplate notice, with the fields enclosed by brackets "[]"
183-
replaced with your own identifying information. (Don't include
184-
the brackets!) The text should be enclosed in the appropriate
185-
comment syntax for the file format. We also recommend that a
186-
file or class name and description of purpose be included on the
187-
same "printed page" as the copyright notice for easier
188-
identification within third-party archives.
189-
190-
Copyright [yyyy] [name of copyright owner]
191-
192-
Licensed under the Apache License, Version 2.0 (the "License");
193-
you may not use this file except in compliance with the License.
194-
You may obtain a copy of the License at
195-
196-
http://www.apache.org/licenses/LICENSE-2.0
197-
198-
Unless required by applicable law or agreed to in writing, software
199-
distributed under the License is distributed on an "AS IS" BASIS,
200-
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
201-
See the License for the specific language governing permissions and
202-
limitations under the License.
43+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
44+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
45+
FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
46+
COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
47+
IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
48+
CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

README.md

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
**Semantic search for [PhysLib](https://physlib.io/) — the formal Lean 4 physics library.**
44

5-
[![License](https://img.shields.io/badge/license-Apache%202.0-blue.svg)](LICENSE)
5+
[![License](https://img.shields.io/badge/license-MIT%20%2B%20Commons%20Clause-blue.svg)](LICENSE)
66
[![Python](https://img.shields.io/badge/python-3.11%2B-blue)](https://www.python.org/)
77
[![Ruff](https://img.shields.io/endpoint?url=https://raw.githubusercontent.com/astral-sh/ruff/main/assets/badge/v2.json)](https://github.com/astral-sh/ruff)
88
[![GitHub](https://img.shields.io/badge/github-Kernel--Science%2Fphyslibsearch-black?logo=github)](https://github.com/Kernel-Science/physlibsearch)
@@ -241,6 +241,14 @@ Contributions are welcome. See [CONTRIBUTING.md](CONTRIBUTING.md) to get started
241241

242242
---
243243

244+
## Next steps
245+
246+
- **Continuous integration** — As PhysLib grows, the database should update automatically when new declarations are merged. The indexing pipeline is designed to be incremental (each SQL step uses `ON CONFLICT DO NOTHING`, and the informalization and embedding steps skip already-processed entries), but this needs to be verified end-to-end for every stage before setting up a CI workflow that triggers on new PhysLib commits.
247+
248+
- **Index QuantumInfo** — The `QuantumInfo` module has not been indexed due to integration issues between PhysLib's QuantumInfo dependencies and jixia. Once resolved, re-running `python -m database jixia` should pick it up without reprocessing the rest of the library.
249+
250+
---
251+
244252
## Acknowledgements
245253

246254
The HyDE query expansion technique is inspired by the [LeanSearch](https://arxiv.org/abs/2403.13310) paper.

frontend/src/app/docs/page.tsx

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -86,6 +86,7 @@ export default function DocsPage() {
8686
["api", "API Reference"],
8787
["self-hosting", "Self-hosting"],
8888
["open-source", "Open source"],
89+
["next-steps", "Next steps"],
8990
].map(([id, label]) => (
9091
<a
9192
key={id}
@@ -282,6 +283,27 @@ uvicorn server:app --host 0.0.0.0 --port 8000`}
282283
/>
283284
</Section>
284285

286+
<Section id="next-steps" title="Next steps">
287+
<ul className="list-disc list-inside flex flex-col gap-3 pl-2">
288+
<li>
289+
<strong>Continuous integration.</strong> As PhysLib grows, the database should update
290+
automatically when new declarations are merged. The indexing pipeline is designed to be
291+
incremental — each SQL step uses{" "}
292+
<code className="font-mono text-xs bg-foreground/8 px-1 py-0.5 rounded">ON CONFLICT DO NOTHING</code>,
293+
and the informalization and embedding steps skip already-processed entries — but this needs
294+
to be verified end-to-end for every stage before wiring up a CI workflow that triggers on
295+
new PhysLib commits.
296+
</li>
297+
<li>
298+
<strong>Index QuantumInfo.</strong> The <code className="font-mono text-xs bg-foreground/8 px-1 py-0.5 rounded">QuantumInfo</code>{" "}
299+
module has not been indexed yet due to integration issues between PhysLib&apos;s QuantumInfo
300+
dependencies and jixia. Once resolved, re-running{" "}
301+
<code className="font-mono text-xs bg-foreground/8 px-1 py-0.5 rounded">python -m database jixia</code>{" "}
302+
should pick it up incrementally without reprocessing the rest of the library.
303+
</li>
304+
</ul>
305+
</Section>
306+
285307
<Section id="open-source" title="Open source">
286308
<p>
287309
PhyslibSearch is open source, built by{" "}

0 commit comments

Comments
 (0)