Compare commits
No commits in common. "dev" and "goal/tactic" have entirely different histories.
dev
...
goal/tacti
804
LICENSE
804
LICENSE
|
|
@ -1,190 +1,674 @@
|
|||
Apache License
|
||||
Version 2.0, January 2004
|
||||
http://www.apache.org/licenses/
|
||||
GNU GENERAL PUBLIC LICENSE
|
||||
Version 3, 29 June 2007
|
||||
|
||||
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
|
||||
Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
|
||||
Everyone is permitted to copy and distribute verbatim copies
|
||||
of this license document, but changing it is not allowed.
|
||||
|
||||
1. Definitions.
|
||||
Preamble
|
||||
|
||||
"License" shall mean the terms and conditions for use, reproduction,
|
||||
and distribution as defined by Sections 1 through 9 of this document.
|
||||
The GNU General Public License is a free, copyleft license for
|
||||
software and other kinds of works.
|
||||
|
||||
"Licensor" shall mean the copyright owner or entity authorized by
|
||||
the copyright owner that is granting the License.
|
||||
The licenses for most software and other practical works are designed
|
||||
to take away your freedom to share and change the works. By contrast,
|
||||
the GNU General Public License is intended to guarantee your freedom to
|
||||
share and change all versions of a program--to make sure it remains free
|
||||
software for all its users. We, the Free Software Foundation, use the
|
||||
GNU General Public License for most of our software; it applies also to
|
||||
any other work released this way by its authors. You can apply it to
|
||||
your programs, too.
|
||||
|
||||
"Legal Entity" shall mean the union of the acting entity and all
|
||||
other entities that control, are controlled by, or are under common
|
||||
control with that entity. For the purposes of this definition,
|
||||
"control" means (i) the power, direct or indirect, to cause the
|
||||
direction or management of such entity, whether by contract or
|
||||
otherwise, or (ii) ownership of fifty percent (50%) or more of the
|
||||
outstanding shares, or (iii) beneficial ownership of such entity.
|
||||
When we speak of free software, we are referring to freedom, not
|
||||
price. Our General Public Licenses are designed to make sure that you
|
||||
have the freedom to distribute copies of free software (and charge for
|
||||
them if you wish), that you receive source code or can get it if you
|
||||
want it, that you can change the software or use pieces of it in new
|
||||
free programs, and that you know you can do these things.
|
||||
|
||||
"You" (or "Your") shall mean an individual or Legal Entity
|
||||
exercising permissions granted by this License.
|
||||
To protect your rights, we need to prevent others from denying you
|
||||
these rights or asking you to surrender the rights. Therefore, you have
|
||||
certain responsibilities if you distribute copies of the software, or if
|
||||
you modify it: responsibilities to respect the freedom of others.
|
||||
|
||||
"Source" form shall mean the preferred form for making modifications,
|
||||
including but not limited to software source code, documentation
|
||||
source, and configuration files.
|
||||
For example, if you distribute copies of such a program, whether
|
||||
gratis or for a fee, you must pass on to the recipients the same
|
||||
freedoms that you received. You must make sure that they, too, receive
|
||||
or can get the source code. And you must show them these terms so they
|
||||
know their rights.
|
||||
|
||||
"Object" form shall mean any form resulting from mechanical
|
||||
transformation or translation of a Source form, including but
|
||||
not limited to compiled object code, generated documentation,
|
||||
and conversions to other media types.
|
||||
Developers that use the GNU GPL protect your rights with two steps:
|
||||
(1) assert copyright on the software, and (2) offer you this License
|
||||
giving you legal permission to copy, distribute and/or modify it.
|
||||
|
||||
"Work" shall mean the work of authorship, whether in Source or
|
||||
Object form, made available under the License, as indicated by a
|
||||
copyright notice that is included in or attached to the work
|
||||
(an example is provided in the Appendix below).
|
||||
For the developers' and authors' protection, the GPL clearly explains
|
||||
that there is no warranty for this free software. For both users' and
|
||||
authors' sake, the GPL requires that modified versions be marked as
|
||||
changed, so that their problems will not be attributed erroneously to
|
||||
authors of previous versions.
|
||||
|
||||
"Derivative Works" shall mean any work, whether in Source or Object
|
||||
form, that is based on (or derived from) the Work and for which the
|
||||
editorial revisions, annotations, elaborations, or other modifications
|
||||
represent, as a whole, an original work of authorship. For the purposes
|
||||
of this License, Derivative Works shall not include works that remain
|
||||
separable from, or merely link (or bind by name) to the interfaces of,
|
||||
the Work and Derivative Works thereof.
|
||||
Some devices are designed to deny users access to install or run
|
||||
modified versions of the software inside them, although the manufacturer
|
||||
can do so. This is fundamentally incompatible with the aim of
|
||||
protecting users' freedom to change the software. The systematic
|
||||
pattern of such abuse occurs in the area of products for individuals to
|
||||
use, which is precisely where it is most unacceptable. Therefore, we
|
||||
have designed this version of the GPL to prohibit the practice for those
|
||||
products. If such problems arise substantially in other domains, we
|
||||
stand ready to extend this provision to those domains in future versions
|
||||
of the GPL, as needed to protect the freedom of users.
|
||||
|
||||
"Contribution" shall mean any work of authorship, including
|
||||
the original version of the Work and any modifications or additions
|
||||
to that Work or Derivative Works thereof, that is intentionally
|
||||
submitted to Licensor for inclusion in the Work by the copyright owner
|
||||
or by an individual or Legal Entity authorized to submit on behalf of
|
||||
the copyright owner. For the purposes of this definition, "submitted"
|
||||
means any form of electronic, verbal, or written communication sent
|
||||
to the Licensor or its representatives, including but not limited to
|
||||
communication on electronic mailing lists, source code control systems,
|
||||
and issue tracking systems that are managed by, or on behalf of, the
|
||||
Licensor for the purpose of discussing and improving the Work, but
|
||||
excluding communication that is conspicuously marked or otherwise
|
||||
designated in writing by the copyright owner as "Not a Contribution."
|
||||
Finally, every program is threatened constantly by software patents.
|
||||
States should not allow patents to restrict development and use of
|
||||
software on general-purpose computers, but in those that do, we wish to
|
||||
avoid the special danger that patents applied to a free program could
|
||||
make it effectively proprietary. To prevent this, the GPL assures that
|
||||
patents cannot be used to render the program non-free.
|
||||
|
||||
"Contributor" shall mean Licensor and any individual or Legal Entity
|
||||
on behalf of whom a Contribution has been received by Licensor and
|
||||
subsequently incorporated within the Work.
|
||||
The precise terms and conditions for copying, distribution and
|
||||
modification follow.
|
||||
|
||||
2. Grant of Copyright License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
copyright license to reproduce, prepare Derivative Works of,
|
||||
publicly display, publicly perform, sublicense, and distribute the
|
||||
Work and such Derivative Works in Source or Object form.
|
||||
TERMS AND CONDITIONS
|
||||
|
||||
3. Grant of Patent License. Subject to the terms and conditions of
|
||||
this License, each Contributor hereby grants to You a perpetual,
|
||||
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
|
||||
(except as stated in this section) patent license to make, have made,
|
||||
use, offer to sell, sell, import, and otherwise transfer the Work,
|
||||
where such license applies only to those patent claims licensable
|
||||
by such Contributor that are necessarily infringed by their
|
||||
Contribution(s) alone or by combination of their Contribution(s)
|
||||
with the Work to which such Contribution(s) was submitted. If You
|
||||
institute patent litigation against any entity (including a
|
||||
cross-claim or counterclaim in a lawsuit) alleging that the Work
|
||||
or a Contribution incorporated within the Work constitutes direct
|
||||
or contributory patent infringement, then any patent licenses
|
||||
granted to You under this License for that Work shall terminate
|
||||
as of the date such litigation is filed.
|
||||
0. Definitions.
|
||||
|
||||
4. Redistribution. You may reproduce and distribute copies of the
|
||||
Work or Derivative Works thereof in any medium, with or without
|
||||
modifications, and in Source or Object form, provided that You
|
||||
meet the following conditions:
|
||||
"This License" refers to version 3 of the GNU General Public License.
|
||||
|
||||
(a) You must give any other recipients of the Work or
|
||||
Derivative Works a copy of this License; and
|
||||
"Copyright" also means copyright-like laws that apply to other kinds of
|
||||
works, such as semiconductor masks.
|
||||
|
||||
(b) You must cause any modified files to carry prominent notices
|
||||
stating that You changed the files; and
|
||||
"The Program" refers to any copyrightable work licensed under this
|
||||
License. Each licensee is addressed as "you". "Licensees" and
|
||||
"recipients" may be individuals or organizations.
|
||||
|
||||
(c) You must retain, in the Source form of any Derivative Works
|
||||
that You distribute, all copyright, patent, trademark, and
|
||||
attribution notices from the Source form of the Work,
|
||||
excluding those notices that do not pertain to any part of
|
||||
the Derivative Works; and
|
||||
To "modify" a work means to copy from or adapt all or part of the work
|
||||
in a fashion requiring copyright permission, other than the making of an
|
||||
exact copy. The resulting work is called a "modified version" of the
|
||||
earlier work or a work "based on" the earlier work.
|
||||
|
||||
(d) If the Work includes a "NOTICE" text file as part of its
|
||||
distribution, then any Derivative Works that You distribute must
|
||||
include a readable copy of the attribution notices contained
|
||||
within such NOTICE file, excluding those notices that do not
|
||||
pertain to any part of the Derivative Works, in at least one
|
||||
of the following places: within a NOTICE text file distributed
|
||||
as part of the Derivative Works; within the Source form or
|
||||
documentation, if provided along with the Derivative Works; or,
|
||||
within a display generated by the Derivative Works, if and
|
||||
wherever such third-party notices normally appear. The contents
|
||||
of the NOTICE file are for informational purposes only and
|
||||
do not modify the License. You may add Your own attribution
|
||||
notices within Derivative Works that You distribute, alongside
|
||||
or as an addendum to the NOTICE text from the Work, provided
|
||||
that such additional attribution notices cannot be construed
|
||||
as modifying the License.
|
||||
A "covered work" means either the unmodified Program or a work based
|
||||
on the Program.
|
||||
|
||||
You may add Your own copyright statement to Your modifications and
|
||||
may provide additional or different license terms and conditions
|
||||
for use, reproduction, or distribution of Your modifications, or
|
||||
for any such Derivative Works as a whole, provided Your use,
|
||||
reproduction, and distribution of the Work otherwise complies with
|
||||
the conditions stated in this License.
|
||||
To "propagate" a work means to do anything with it that, without
|
||||
permission, would make you directly or secondarily liable for
|
||||
infringement under applicable copyright law, except executing it on a
|
||||
computer or modifying a private copy. Propagation includes copying,
|
||||
distribution (with or without modification), making available to the
|
||||
public, and in some countries other activities as well.
|
||||
|
||||
5. Submission of Contributions. Unless You explicitly state otherwise,
|
||||
any Contribution intentionally submitted for inclusion in the Work
|
||||
by You to the Licensor shall be under the terms and conditions of
|
||||
this License, without any additional terms or conditions.
|
||||
Notwithstanding the above, nothing herein shall supersede or modify
|
||||
the terms of any separate license agreement you may have executed
|
||||
with Licensor regarding such Contributions.
|
||||
To "convey" a work means any kind of propagation that enables other
|
||||
parties to make or receive copies. Mere interaction with a user through
|
||||
a computer network, with no transfer of a copy, is not conveying.
|
||||
|
||||
6. Trademarks. This License does not grant permission to use the trade
|
||||
names, trademarks, service marks, or product names of the Licensor,
|
||||
except as required for reasonable and customary use in describing the
|
||||
origin of the Work and reproducing the content of the NOTICE file.
|
||||
An interactive user interface displays "Appropriate Legal Notices"
|
||||
to the extent that it includes a convenient and prominently visible
|
||||
feature that (1) displays an appropriate copyright notice, and (2)
|
||||
tells the user that there is no warranty for the work (except to the
|
||||
extent that warranties are provided), that licensees may convey the
|
||||
work under this License, and how to view a copy of this License. If
|
||||
the interface presents a list of user commands or options, such as a
|
||||
menu, a prominent item in the list meets this criterion.
|
||||
|
||||
7. Disclaimer of Warranty. Unless required by applicable law or
|
||||
agreed to in writing, Licensor provides the Work (and each
|
||||
Contributor provides its Contributions) on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
|
||||
implied, including, without limitation, any warranties or conditions
|
||||
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
|
||||
PARTICULAR PURPOSE. You are solely responsible for determining the
|
||||
appropriateness of using or redistributing the Work and assume any
|
||||
risks associated with Your exercise of permissions under this License.
|
||||
1. Source Code.
|
||||
|
||||
8. Limitation of Liability. In no event and under no legal theory,
|
||||
whether in tort (including negligence), contract, or otherwise,
|
||||
unless required by applicable law (such as deliberate and grossly
|
||||
negligent acts) or agreed to in writing, shall any Contributor be
|
||||
liable to You for damages, including any direct, indirect, special,
|
||||
incidental, or consequential damages of any character arising as a
|
||||
result of this License or out of the use or inability to use the
|
||||
Work (including but not limited to damages for loss of goodwill,
|
||||
work stoppage, computer failure or malfunction, or any and all
|
||||
other commercial damages or losses), even if such Contributor
|
||||
has been advised of the possibility of such damages.
|
||||
The "source code" for a work means the preferred form of the work
|
||||
for making modifications to it. "Object code" means any non-source
|
||||
form of a work.
|
||||
|
||||
9. Accepting Warranty or Additional Liability. While redistributing
|
||||
the Work or Derivative Works thereof, You may choose to offer,
|
||||
and charge a fee for, acceptance of support, warranty, indemnity,
|
||||
or other liability obligations and/or rights consistent with this
|
||||
License. However, in accepting such obligations, You may act only
|
||||
on Your own behalf and on Your sole responsibility, not on behalf
|
||||
of any other Contributor, and only if You agree to indemnify,
|
||||
defend, and hold each Contributor harmless for any liability
|
||||
incurred by, or claims asserted against, such Contributor by reason
|
||||
of your accepting any such warranty or additional liability.
|
||||
A "Standard Interface" means an interface that either is an official
|
||||
standard defined by a recognized standards body, or, in the case of
|
||||
interfaces specified for a particular programming language, one that
|
||||
is widely used among developers working in that language.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
The "System Libraries" of an executable work include anything, other
|
||||
than the work as a whole, that (a) is included in the normal form of
|
||||
packaging a Major Component, but which is not part of that Major
|
||||
Component, and (b) serves only to enable use of the work with that
|
||||
Major Component, or to implement a Standard Interface for which an
|
||||
implementation is available to the public in source code form. A
|
||||
"Major Component", in this context, means a major essential component
|
||||
(kernel, window system, and so on) of the specific operating system
|
||||
(if any) on which the executable work runs, or a compiler used to
|
||||
produce the work, or an object code interpreter used to run it.
|
||||
|
||||
Copyright 2024 Leni Aniva
|
||||
The "Corresponding Source" for a work in object code form means all
|
||||
the source code needed to generate, install, and (for an executable
|
||||
work) run the object code and to modify the work, including scripts to
|
||||
control those activities. However, it does not include the work's
|
||||
System Libraries, or general-purpose tools or generally available free
|
||||
programs which are used unmodified in performing those activities but
|
||||
which are not part of the work. For example, Corresponding Source
|
||||
includes interface definition files associated with source files for
|
||||
the work, and the source code for shared libraries and dynamically
|
||||
linked subprograms that the work is specifically designed to require,
|
||||
such as by intimate data communication or control flow between those
|
||||
subprograms and other parts of the work.
|
||||
|
||||
Licensed under the Apache License, Version 2.0 (the "License");
|
||||
you may not use this file except in compliance with the License.
|
||||
You may obtain a copy of the License at
|
||||
The Corresponding Source need not include anything that users
|
||||
can regenerate automatically from other parts of the Corresponding
|
||||
Source.
|
||||
|
||||
http://www.apache.org/licenses/LICENSE-2.0
|
||||
The Corresponding Source for a work in source code form is that
|
||||
same work.
|
||||
|
||||
Unless required by applicable law or agreed to in writing, software
|
||||
distributed under the License is distributed on an "AS IS" BASIS,
|
||||
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
||||
See the License for the specific language governing permissions and
|
||||
limitations under the License.
|
||||
2. Basic Permissions.
|
||||
|
||||
All rights granted under this License are granted for the term of
|
||||
copyright on the Program, and are irrevocable provided the stated
|
||||
conditions are met. This License explicitly affirms your unlimited
|
||||
permission to run the unmodified Program. The output from running a
|
||||
covered work is covered by this License only if the output, given its
|
||||
content, constitutes a covered work. This License acknowledges your
|
||||
rights of fair use or other equivalent, as provided by copyright law.
|
||||
|
||||
You may make, run and propagate covered works that you do not
|
||||
convey, without conditions so long as your license otherwise remains
|
||||
in force. You may convey covered works to others for the sole purpose
|
||||
of having them make modifications exclusively for you, or provide you
|
||||
with facilities for running those works, provided that you comply with
|
||||
the terms of this License in conveying all material for which you do
|
||||
not control copyright. Those thus making or running the covered works
|
||||
for you must do so exclusively on your behalf, under your direction
|
||||
and control, on terms that prohibit them from making any copies of
|
||||
your copyrighted material outside their relationship with you.
|
||||
|
||||
Conveying under any other circumstances is permitted solely under
|
||||
the conditions stated below. Sublicensing is not allowed; section 10
|
||||
makes it unnecessary.
|
||||
|
||||
3. Protecting Users' Legal Rights From Anti-Circumvention Law.
|
||||
|
||||
No covered work shall be deemed part of an effective technological
|
||||
measure under any applicable law fulfilling obligations under article
|
||||
11 of the WIPO copyright treaty adopted on 20 December 1996, or
|
||||
similar laws prohibiting or restricting circumvention of such
|
||||
measures.
|
||||
|
||||
When you convey a covered work, you waive any legal power to forbid
|
||||
circumvention of technological measures to the extent such circumvention
|
||||
is effected by exercising rights under this License with respect to
|
||||
the covered work, and you disclaim any intention to limit operation or
|
||||
modification of the work as a means of enforcing, against the work's
|
||||
users, your or third parties' legal rights to forbid circumvention of
|
||||
technological measures.
|
||||
|
||||
4. Conveying Verbatim Copies.
|
||||
|
||||
You may convey verbatim copies of the Program's source code as you
|
||||
receive it, in any medium, provided that you conspicuously and
|
||||
appropriately publish on each copy an appropriate copyright notice;
|
||||
keep intact all notices stating that this License and any
|
||||
non-permissive terms added in accord with section 7 apply to the code;
|
||||
keep intact all notices of the absence of any warranty; and give all
|
||||
recipients a copy of this License along with the Program.
|
||||
|
||||
You may charge any price or no price for each copy that you convey,
|
||||
and you may offer support or warranty protection for a fee.
|
||||
|
||||
5. Conveying Modified Source Versions.
|
||||
|
||||
You may convey a work based on the Program, or the modifications to
|
||||
produce it from the Program, in the form of source code under the
|
||||
terms of section 4, provided that you also meet all of these conditions:
|
||||
|
||||
a) The work must carry prominent notices stating that you modified
|
||||
it, and giving a relevant date.
|
||||
|
||||
b) The work must carry prominent notices stating that it is
|
||||
released under this License and any conditions added under section
|
||||
7. This requirement modifies the requirement in section 4 to
|
||||
"keep intact all notices".
|
||||
|
||||
c) You must license the entire work, as a whole, under this
|
||||
License to anyone who comes into possession of a copy. This
|
||||
License will therefore apply, along with any applicable section 7
|
||||
additional terms, to the whole of the work, and all its parts,
|
||||
regardless of how they are packaged. This License gives no
|
||||
permission to license the work in any other way, but it does not
|
||||
invalidate such permission if you have separately received it.
|
||||
|
||||
d) If the work has interactive user interfaces, each must display
|
||||
Appropriate Legal Notices; however, if the Program has interactive
|
||||
interfaces that do not display Appropriate Legal Notices, your
|
||||
work need not make them do so.
|
||||
|
||||
A compilation of a covered work with other separate and independent
|
||||
works, which are not by their nature extensions of the covered work,
|
||||
and which are not combined with it such as to form a larger program,
|
||||
in or on a volume of a storage or distribution medium, is called an
|
||||
"aggregate" if the compilation and its resulting copyright are not
|
||||
used to limit the access or legal rights of the compilation's users
|
||||
beyond what the individual works permit. Inclusion of a covered work
|
||||
in an aggregate does not cause this License to apply to the other
|
||||
parts of the aggregate.
|
||||
|
||||
6. Conveying Non-Source Forms.
|
||||
|
||||
You may convey a covered work in object code form under the terms
|
||||
of sections 4 and 5, provided that you also convey the
|
||||
machine-readable Corresponding Source under the terms of this License,
|
||||
in one of these ways:
|
||||
|
||||
a) Convey the object code in, or embodied in, a physical product
|
||||
(including a physical distribution medium), accompanied by the
|
||||
Corresponding Source fixed on a durable physical medium
|
||||
customarily used for software interchange.
|
||||
|
||||
b) Convey the object code in, or embodied in, a physical product
|
||||
(including a physical distribution medium), accompanied by a
|
||||
written offer, valid for at least three years and valid for as
|
||||
long as you offer spare parts or customer support for that product
|
||||
model, to give anyone who possesses the object code either (1) a
|
||||
copy of the Corresponding Source for all the software in the
|
||||
product that is covered by this License, on a durable physical
|
||||
medium customarily used for software interchange, for a price no
|
||||
more than your reasonable cost of physically performing this
|
||||
conveying of source, or (2) access to copy the
|
||||
Corresponding Source from a network server at no charge.
|
||||
|
||||
c) Convey individual copies of the object code with a copy of the
|
||||
written offer to provide the Corresponding Source. This
|
||||
alternative is allowed only occasionally and noncommercially, and
|
||||
only if you received the object code with such an offer, in accord
|
||||
with subsection 6b.
|
||||
|
||||
d) Convey the object code by offering access from a designated
|
||||
place (gratis or for a charge), and offer equivalent access to the
|
||||
Corresponding Source in the same way through the same place at no
|
||||
further charge. You need not require recipients to copy the
|
||||
Corresponding Source along with the object code. If the place to
|
||||
copy the object code is a network server, the Corresponding Source
|
||||
may be on a different server (operated by you or a third party)
|
||||
that supports equivalent copying facilities, provided you maintain
|
||||
clear directions next to the object code saying where to find the
|
||||
Corresponding Source. Regardless of what server hosts the
|
||||
Corresponding Source, you remain obligated to ensure that it is
|
||||
available for as long as needed to satisfy these requirements.
|
||||
|
||||
e) Convey the object code using peer-to-peer transmission, provided
|
||||
you inform other peers where the object code and Corresponding
|
||||
Source of the work are being offered to the general public at no
|
||||
charge under subsection 6d.
|
||||
|
||||
A separable portion of the object code, whose source code is excluded
|
||||
from the Corresponding Source as a System Library, need not be
|
||||
included in conveying the object code work.
|
||||
|
||||
A "User Product" is either (1) a "consumer product", which means any
|
||||
tangible personal property which is normally used for personal, family,
|
||||
or household purposes, or (2) anything designed or sold for incorporation
|
||||
into a dwelling. In determining whether a product is a consumer product,
|
||||
doubtful cases shall be resolved in favor of coverage. For a particular
|
||||
product received by a particular user, "normally used" refers to a
|
||||
typical or common use of that class of product, regardless of the status
|
||||
of the particular user or of the way in which the particular user
|
||||
actually uses, or expects or is expected to use, the product. A product
|
||||
is a consumer product regardless of whether the product has substantial
|
||||
commercial, industrial or non-consumer uses, unless such uses represent
|
||||
the only significant mode of use of the product.
|
||||
|
||||
"Installation Information" for a User Product means any methods,
|
||||
procedures, authorization keys, or other information required to install
|
||||
and execute modified versions of a covered work in that User Product from
|
||||
a modified version of its Corresponding Source. The information must
|
||||
suffice to ensure that the continued functioning of the modified object
|
||||
code is in no case prevented or interfered with solely because
|
||||
modification has been made.
|
||||
|
||||
If you convey an object code work under this section in, or with, or
|
||||
specifically for use in, a User Product, and the conveying occurs as
|
||||
part of a transaction in which the right of possession and use of the
|
||||
User Product is transferred to the recipient in perpetuity or for a
|
||||
fixed term (regardless of how the transaction is characterized), the
|
||||
Corresponding Source conveyed under this section must be accompanied
|
||||
by the Installation Information. But this requirement does not apply
|
||||
if neither you nor any third party retains the ability to install
|
||||
modified object code on the User Product (for example, the work has
|
||||
been installed in ROM).
|
||||
|
||||
The requirement to provide Installation Information does not include a
|
||||
requirement to continue to provide support service, warranty, or updates
|
||||
for a work that has been modified or installed by the recipient, or for
|
||||
the User Product in which it has been modified or installed. Access to a
|
||||
network may be denied when the modification itself materially and
|
||||
adversely affects the operation of the network or violates the rules and
|
||||
protocols for communication across the network.
|
||||
|
||||
Corresponding Source conveyed, and Installation Information provided,
|
||||
in accord with this section must be in a format that is publicly
|
||||
documented (and with an implementation available to the public in
|
||||
source code form), and must require no special password or key for
|
||||
unpacking, reading or copying.
|
||||
|
||||
7. Additional Terms.
|
||||
|
||||
"Additional permissions" are terms that supplement the terms of this
|
||||
License by making exceptions from one or more of its conditions.
|
||||
Additional permissions that are applicable to the entire Program shall
|
||||
be treated as though they were included in this License, to the extent
|
||||
that they are valid under applicable law. If additional permissions
|
||||
apply only to part of the Program, that part may be used separately
|
||||
under those permissions, but the entire Program remains governed by
|
||||
this License without regard to the additional permissions.
|
||||
|
||||
When you convey a copy of a covered work, you may at your option
|
||||
remove any additional permissions from that copy, or from any part of
|
||||
it. (Additional permissions may be written to require their own
|
||||
removal in certain cases when you modify the work.) You may place
|
||||
additional permissions on material, added by you to a covered work,
|
||||
for which you have or can give appropriate copyright permission.
|
||||
|
||||
Notwithstanding any other provision of this License, for material you
|
||||
add to a covered work, you may (if authorized by the copyright holders of
|
||||
that material) supplement the terms of this License with terms:
|
||||
|
||||
a) Disclaiming warranty or limiting liability differently from the
|
||||
terms of sections 15 and 16 of this License; or
|
||||
|
||||
b) Requiring preservation of specified reasonable legal notices or
|
||||
author attributions in that material or in the Appropriate Legal
|
||||
Notices displayed by works containing it; or
|
||||
|
||||
c) Prohibiting misrepresentation of the origin of that material, or
|
||||
requiring that modified versions of such material be marked in
|
||||
reasonable ways as different from the original version; or
|
||||
|
||||
d) Limiting the use for publicity purposes of names of licensors or
|
||||
authors of the material; or
|
||||
|
||||
e) Declining to grant rights under trademark law for use of some
|
||||
trade names, trademarks, or service marks; or
|
||||
|
||||
f) Requiring indemnification of licensors and authors of that
|
||||
material by anyone who conveys the material (or modified versions of
|
||||
it) with contractual assumptions of liability to the recipient, for
|
||||
any liability that these contractual assumptions directly impose on
|
||||
those licensors and authors.
|
||||
|
||||
All other non-permissive additional terms are considered "further
|
||||
restrictions" within the meaning of section 10. If the Program as you
|
||||
received it, or any part of it, contains a notice stating that it is
|
||||
governed by this License along with a term that is a further
|
||||
restriction, you may remove that term. If a license document contains
|
||||
a further restriction but permits relicensing or conveying under this
|
||||
License, you may add to a covered work material governed by the terms
|
||||
of that license document, provided that the further restriction does
|
||||
not survive such relicensing or conveying.
|
||||
|
||||
If you add terms to a covered work in accord with this section, you
|
||||
must place, in the relevant source files, a statement of the
|
||||
additional terms that apply to those files, or a notice indicating
|
||||
where to find the applicable terms.
|
||||
|
||||
Additional terms, permissive or non-permissive, may be stated in the
|
||||
form of a separately written license, or stated as exceptions;
|
||||
the above requirements apply either way.
|
||||
|
||||
8. Termination.
|
||||
|
||||
You may not propagate or modify a covered work except as expressly
|
||||
provided under this License. Any attempt otherwise to propagate or
|
||||
modify it is void, and will automatically terminate your rights under
|
||||
this License (including any patent licenses granted under the third
|
||||
paragraph of section 11).
|
||||
|
||||
However, if you cease all violation of this License, then your
|
||||
license from a particular copyright holder is reinstated (a)
|
||||
provisionally, unless and until the copyright holder explicitly and
|
||||
finally terminates your license, and (b) permanently, if the copyright
|
||||
holder fails to notify you of the violation by some reasonable means
|
||||
prior to 60 days after the cessation.
|
||||
|
||||
Moreover, your license from a particular copyright holder is
|
||||
reinstated permanently if the copyright holder notifies you of the
|
||||
violation by some reasonable means, this is the first time you have
|
||||
received notice of violation of this License (for any work) from that
|
||||
copyright holder, and you cure the violation prior to 30 days after
|
||||
your receipt of the notice.
|
||||
|
||||
Termination of your rights under this section does not terminate the
|
||||
licenses of parties who have received copies or rights from you under
|
||||
this License. If your rights have been terminated and not permanently
|
||||
reinstated, you do not qualify to receive new licenses for the same
|
||||
material under section 10.
|
||||
|
||||
9. Acceptance Not Required for Having Copies.
|
||||
|
||||
You are not required to accept this License in order to receive or
|
||||
run a copy of the Program. Ancillary propagation of a covered work
|
||||
occurring solely as a consequence of using peer-to-peer transmission
|
||||
to receive a copy likewise does not require acceptance. However,
|
||||
nothing other than this License grants you permission to propagate or
|
||||
modify any covered work. These actions infringe copyright if you do
|
||||
not accept this License. Therefore, by modifying or propagating a
|
||||
covered work, you indicate your acceptance of this License to do so.
|
||||
|
||||
10. Automatic Licensing of Downstream Recipients.
|
||||
|
||||
Each time you convey a covered work, the recipient automatically
|
||||
receives a license from the original licensors, to run, modify and
|
||||
propagate that work, subject to this License. You are not responsible
|
||||
for enforcing compliance by third parties with this License.
|
||||
|
||||
An "entity transaction" is a transaction transferring control of an
|
||||
organization, or substantially all assets of one, or subdividing an
|
||||
organization, or merging organizations. If propagation of a covered
|
||||
work results from an entity transaction, each party to that
|
||||
transaction who receives a copy of the work also receives whatever
|
||||
licenses to the work the party's predecessor in interest had or could
|
||||
give under the previous paragraph, plus a right to possession of the
|
||||
Corresponding Source of the work from the predecessor in interest, if
|
||||
the predecessor has it or can get it with reasonable efforts.
|
||||
|
||||
You may not impose any further restrictions on the exercise of the
|
||||
rights granted or affirmed under this License. For example, you may
|
||||
not impose a license fee, royalty, or other charge for exercise of
|
||||
rights granted under this License, and you may not initiate litigation
|
||||
(including a cross-claim or counterclaim in a lawsuit) alleging that
|
||||
any patent claim is infringed by making, using, selling, offering for
|
||||
sale, or importing the Program or any portion of it.
|
||||
|
||||
11. Patents.
|
||||
|
||||
A "contributor" is a copyright holder who authorizes use under this
|
||||
License of the Program or a work on which the Program is based. The
|
||||
work thus licensed is called the contributor's "contributor version".
|
||||
|
||||
A contributor's "essential patent claims" are all patent claims
|
||||
owned or controlled by the contributor, whether already acquired or
|
||||
hereafter acquired, that would be infringed by some manner, permitted
|
||||
by this License, of making, using, or selling its contributor version,
|
||||
but do not include claims that would be infringed only as a
|
||||
consequence of further modification of the contributor version. For
|
||||
purposes of this definition, "control" includes the right to grant
|
||||
patent sublicenses in a manner consistent with the requirements of
|
||||
this License.
|
||||
|
||||
Each contributor grants you a non-exclusive, worldwide, royalty-free
|
||||
patent license under the contributor's essential patent claims, to
|
||||
make, use, sell, offer for sale, import and otherwise run, modify and
|
||||
propagate the contents of its contributor version.
|
||||
|
||||
In the following three paragraphs, a "patent license" is any express
|
||||
agreement or commitment, however denominated, not to enforce a patent
|
||||
(such as an express permission to practice a patent or covenant not to
|
||||
sue for patent infringement). To "grant" such a patent license to a
|
||||
party means to make such an agreement or commitment not to enforce a
|
||||
patent against the party.
|
||||
|
||||
If you convey a covered work, knowingly relying on a patent license,
|
||||
and the Corresponding Source of the work is not available for anyone
|
||||
to copy, free of charge and under the terms of this License, through a
|
||||
publicly available network server or other readily accessible means,
|
||||
then you must either (1) cause the Corresponding Source to be so
|
||||
available, or (2) arrange to deprive yourself of the benefit of the
|
||||
patent license for this particular work, or (3) arrange, in a manner
|
||||
consistent with the requirements of this License, to extend the patent
|
||||
license to downstream recipients. "Knowingly relying" means you have
|
||||
actual knowledge that, but for the patent license, your conveying the
|
||||
covered work in a country, or your recipient's use of the covered work
|
||||
in a country, would infringe one or more identifiable patents in that
|
||||
country that you have reason to believe are valid.
|
||||
|
||||
If, pursuant to or in connection with a single transaction or
|
||||
arrangement, you convey, or propagate by procuring conveyance of, a
|
||||
covered work, and grant a patent license to some of the parties
|
||||
receiving the covered work authorizing them to use, propagate, modify
|
||||
or convey a specific copy of the covered work, then the patent license
|
||||
you grant is automatically extended to all recipients of the covered
|
||||
work and works based on it.
|
||||
|
||||
A patent license is "discriminatory" if it does not include within
|
||||
the scope of its coverage, prohibits the exercise of, or is
|
||||
conditioned on the non-exercise of one or more of the rights that are
|
||||
specifically granted under this License. You may not convey a covered
|
||||
work if you are a party to an arrangement with a third party that is
|
||||
in the business of distributing software, under which you make payment
|
||||
to the third party based on the extent of your activity of conveying
|
||||
the work, and under which the third party grants, to any of the
|
||||
parties who would receive the covered work from you, a discriminatory
|
||||
patent license (a) in connection with copies of the covered work
|
||||
conveyed by you (or copies made from those copies), or (b) primarily
|
||||
for and in connection with specific products or compilations that
|
||||
contain the covered work, unless you entered into that arrangement,
|
||||
or that patent license was granted, prior to 28 March 2007.
|
||||
|
||||
Nothing in this License shall be construed as excluding or limiting
|
||||
any implied license or other defenses to infringement that may
|
||||
otherwise be available to you under applicable patent law.
|
||||
|
||||
12. No Surrender of Others' Freedom.
|
||||
|
||||
If conditions are imposed on you (whether by court order, agreement or
|
||||
otherwise) that contradict the conditions of this License, they do not
|
||||
excuse you from the conditions of this License. If you cannot convey a
|
||||
covered work so as to satisfy simultaneously your obligations under this
|
||||
License and any other pertinent obligations, then as a consequence you may
|
||||
not convey it at all. For example, if you agree to terms that obligate you
|
||||
to collect a royalty for further conveying from those to whom you convey
|
||||
the Program, the only way you could satisfy both those terms and this
|
||||
License would be to refrain entirely from conveying the Program.
|
||||
|
||||
13. Use with the GNU Affero General Public License.
|
||||
|
||||
Notwithstanding any other provision of this License, you have
|
||||
permission to link or combine any covered work with a work licensed
|
||||
under version 3 of the GNU Affero General Public License into a single
|
||||
combined work, and to convey the resulting work. The terms of this
|
||||
License will continue to apply to the part which is the covered work,
|
||||
but the special requirements of the GNU Affero General Public License,
|
||||
section 13, concerning interaction through a network will apply to the
|
||||
combination as such.
|
||||
|
||||
14. Revised Versions of this License.
|
||||
|
||||
The Free Software Foundation may publish revised and/or new versions of
|
||||
the GNU General Public License from time to time. Such new versions will
|
||||
be similar in spirit to the present version, but may differ in detail to
|
||||
address new problems or concerns.
|
||||
|
||||
Each version is given a distinguishing version number. If the
|
||||
Program specifies that a certain numbered version of the GNU General
|
||||
Public License "or any later version" applies to it, you have the
|
||||
option of following the terms and conditions either of that numbered
|
||||
version or of any later version published by the Free Software
|
||||
Foundation. If the Program does not specify a version number of the
|
||||
GNU General Public License, you may choose any version ever published
|
||||
by the Free Software Foundation.
|
||||
|
||||
If the Program specifies that a proxy can decide which future
|
||||
versions of the GNU General Public License can be used, that proxy's
|
||||
public statement of acceptance of a version permanently authorizes you
|
||||
to choose that version for the Program.
|
||||
|
||||
Later license versions may give you additional or different
|
||||
permissions. However, no additional obligations are imposed on any
|
||||
author or copyright holder as a result of your choosing to follow a
|
||||
later version.
|
||||
|
||||
15. Disclaimer of Warranty.
|
||||
|
||||
THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
|
||||
APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
|
||||
HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
|
||||
OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
|
||||
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
|
||||
PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
|
||||
IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
|
||||
ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
|
||||
|
||||
16. Limitation of Liability.
|
||||
|
||||
IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
|
||||
WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
|
||||
THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
|
||||
GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
|
||||
USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
|
||||
DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
|
||||
PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
|
||||
EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
|
||||
SUCH DAMAGES.
|
||||
|
||||
17. Interpretation of Sections 15 and 16.
|
||||
|
||||
If the disclaimer of warranty and limitation of liability provided
|
||||
above cannot be given local legal effect according to their terms,
|
||||
reviewing courts shall apply local law that most closely approximates
|
||||
an absolute waiver of all civil liability in connection with the
|
||||
Program, unless a warranty or assumption of liability accompanies a
|
||||
copy of the Program in return for a fee.
|
||||
|
||||
END OF TERMS AND CONDITIONS
|
||||
|
||||
How to Apply These Terms to Your New Programs
|
||||
|
||||
If you develop a new program, and you want it to be of the greatest
|
||||
possible use to the public, the best way to achieve this is to make it
|
||||
free software which everyone can redistribute and change under these terms.
|
||||
|
||||
To do so, attach the following notices to the program. It is safest
|
||||
to attach them to the start of each source file to most effectively
|
||||
state the exclusion of warranty; and each file should have at least
|
||||
the "copyright" line and a pointer to where the full notice is found.
|
||||
|
||||
<one line to give the program's name and a brief idea of what it does.>
|
||||
Copyright (C) <year> <name of author>
|
||||
|
||||
This program is free software: you can redistribute it and/or modify
|
||||
it under the terms of the GNU General Public License as published by
|
||||
the Free Software Foundation, either version 3 of the License, or
|
||||
(at your option) any later version.
|
||||
|
||||
This program is distributed in the hope that it will be useful,
|
||||
but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
GNU General Public License for more details.
|
||||
|
||||
You should have received a copy of the GNU General Public License
|
||||
along with this program. If not, see <https://www.gnu.org/licenses/>.
|
||||
|
||||
Also add information on how to contact you by electronic and paper mail.
|
||||
|
||||
If the program does terminal interaction, make it output a short
|
||||
notice like this when it starts in an interactive mode:
|
||||
|
||||
<program> Copyright (C) <year> <name of author>
|
||||
This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
|
||||
This is free software, and you are welcome to redistribute it
|
||||
under certain conditions; type `show c' for details.
|
||||
|
||||
The hypothetical commands `show w' and `show c' should show the appropriate
|
||||
parts of the General Public License. Of course, your program's commands
|
||||
might be different; for a GUI interface, you would use an "about box".
|
||||
|
||||
You should also get your employer (if you work as a programmer) or school,
|
||||
if any, to sign a "copyright disclaimer" for the program, if necessary.
|
||||
For more information on this, and how to apply and follow the GNU GPL, see
|
||||
<https://www.gnu.org/licenses/>.
|
||||
|
||||
The GNU General Public License does not permit incorporating your program
|
||||
into proprietary programs. If your program is a subroutine library, you
|
||||
may consider it more useful to permit linking proprietary applications with
|
||||
the library. If this is what you want to do, use the GNU Lesser General
|
||||
Public License instead of this License. But first, please read
|
||||
<https://www.gnu.org/licenses/why-not-lgpl.html>.
|
||||
|
|
|
|||
37
Main.lean
37
Main.lean
|
|
@ -1,15 +1,16 @@
|
|||
import Lean.Data.Json
|
||||
import Lean.Environment
|
||||
|
||||
import Pantograph.Version
|
||||
import Pantograph.Library
|
||||
import Pantograph
|
||||
import Repl
|
||||
|
||||
-- Main IO functions
|
||||
open Pantograph.Repl
|
||||
open Pantograph.Protocol
|
||||
open Pantograph
|
||||
|
||||
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
|
||||
def parseCommand (s: String): Except String Command := do
|
||||
def parseCommand (s: String): Except String Protocol.Command := do
|
||||
let s := s.trim
|
||||
match s.get? 0 with
|
||||
| .some '{' => -- Parse in Json mode
|
||||
|
|
@ -29,20 +30,15 @@ partial def loop : MainM Unit := do
|
|||
if command.trim.length = 0 then return ()
|
||||
match parseCommand command with
|
||||
| .error error =>
|
||||
let error := Lean.toJson ({ error := "command", desc := error }: InteractionError)
|
||||
let error := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
|
||||
-- Using `Lean.Json.compress` here to prevent newline
|
||||
IO.println error.compress
|
||||
| .ok command =>
|
||||
try
|
||||
let ret ← execute command
|
||||
let str := match state.options.printJsonPretty with
|
||||
| true => ret.pretty
|
||||
| false => ret.compress
|
||||
IO.println str
|
||||
catch e =>
|
||||
let message ← e.toMessageData.toString
|
||||
let error := Lean.toJson ({ error := "main", desc := message }: InteractionError)
|
||||
IO.println error.compress
|
||||
let ret ← execute command
|
||||
let str := match state.options.printJsonPretty with
|
||||
| true => ret.pretty
|
||||
| false => ret.compress
|
||||
IO.println str
|
||||
loop
|
||||
|
||||
|
||||
|
|
@ -50,15 +46,15 @@ unsafe def main (args: List String): IO Unit := do
|
|||
-- NOTE: A more sophisticated scheme of command line argument handling is needed.
|
||||
-- Separate imports and options
|
||||
if args == ["--version"] then do
|
||||
IO.println s!"{Pantograph.version}"
|
||||
println! s!"{version}"
|
||||
return
|
||||
|
||||
Pantograph.initSearch ""
|
||||
initSearch ""
|
||||
|
||||
let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
|
||||
|>.toArray |> Pantograph.createCoreContext
|
||||
|>.toArray |> createCoreContext
|
||||
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
|
||||
let coreState ← Pantograph.createCoreState imports.toArray
|
||||
let coreState ← createCoreState imports.toArray
|
||||
let context: Context := {
|
||||
imports
|
||||
}
|
||||
|
|
@ -67,6 +63,5 @@ unsafe def main (args: List String): IO Unit := do
|
|||
IO.println "ready."
|
||||
discard <| coreM.toIO coreContext coreState
|
||||
catch ex =>
|
||||
let message := ex.toString
|
||||
let error := Lean.toJson ({ error := "io", desc := message }: InteractionError)
|
||||
IO.println error.compress
|
||||
IO.println "Uncaught IO exception"
|
||||
IO.println ex.toString
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
import Pantograph.Delate
|
||||
import Pantograph.Elab
|
||||
import Pantograph.Compile
|
||||
import Pantograph.Condensed
|
||||
import Pantograph.Environment
|
||||
import Pantograph.Frontend
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Library
|
||||
import Pantograph.Protocol
|
||||
|
|
|
|||
|
|
@ -0,0 +1,25 @@
|
|||
/- Adapted from lean-training-data by semorrison -/
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Compile.Frontend
|
||||
import Pantograph.Compile.Elab
|
||||
import Pantograph.Compile.Parse
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Compile
|
||||
|
||||
def collectTacticsFromCompilation (steps : List CompilationStep) : IO (List Protocol.InvokedTactic) := do
|
||||
let infoTrees := steps.bind (·.trees)
|
||||
let tacticInfoTrees := infoTrees.bind λ tree => tree.filter λ
|
||||
| info@(.ofTacticInfo _) => info.isOriginal
|
||||
| _ => false
|
||||
let tactics := tacticInfoTrees.bind collectTactics
|
||||
tactics.mapM λ invocation => do
|
||||
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
|
||||
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
|
||||
let tactic ← invocation.ctx.runMetaM {} do
|
||||
let t ← Lean.PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
|
||||
return t.pretty
|
||||
return { goalBefore, goalAfter, tactic }
|
||||
|
||||
end Pantograph.Compile
|
||||
|
|
@ -1,12 +1,9 @@
|
|||
/- Adapted from https://github.com/semorrison/lean-training-data -/
|
||||
|
||||
import Lean.Elab.Import
|
||||
import Lean.Elab.Command
|
||||
import Lean.Elab.InfoTree
|
||||
|
||||
import Pantograph.Frontend.Basic
|
||||
import Pantograph.Frontend.MetaTranslate
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Compile.Frontend
|
||||
|
||||
open Lean
|
||||
|
||||
|
|
@ -78,7 +75,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
|
|||
end Lean.Elab.InfoTree
|
||||
|
||||
|
||||
namespace Pantograph.Frontend
|
||||
namespace Pantograph.Compile
|
||||
|
||||
-- Info tree filtering functions
|
||||
|
||||
|
|
@ -89,7 +86,6 @@ structure TacticInvocation where
|
|||
namespace TacticInvocation
|
||||
|
||||
/-- Return the range of the tactic, as a pair of file positions. -/
|
||||
@[export pantograph_frontend_tactic_invocation_range]
|
||||
protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx
|
||||
|
||||
/-- Pretty print a tactic. -/
|
||||
|
|
@ -122,27 +118,20 @@ protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
|
|||
protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
|
||||
t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
|
||||
|
||||
protected def usedConstants (t: TacticInvocation) : NameSet :=
|
||||
let info := t.info
|
||||
info.goalsBefore
|
||||
|>.filterMap info.mctxAfter.getExprAssignmentCore?
|
||||
|>.map Expr.getUsedConstantsAsSet
|
||||
|>.foldl .union .empty
|
||||
|
||||
end TacticInvocation
|
||||
|
||||
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
|
||||
partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
|
||||
partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
|
||||
List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
|
||||
match t with
|
||||
| .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
|
||||
| .context inner t => findAllInfo t (inner.mergeIntoOuter? ctx) pred
|
||||
| .node i children =>
|
||||
(if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
|
||||
(if pred i then [(i, ctx, children)] else []) ++ children.toList.bind (fun t => findAllInfo t ctx pred)
|
||||
| _ => []
|
||||
|
||||
/-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
|
||||
each equipped with its relevant `ContextInfo`, and any children info trees. -/
|
||||
private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
|
||||
def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
|
||||
let infos := findAllInfo t none fun i => match i with
|
||||
| .ofTacticInfo _ => true
|
||||
| _ => false
|
||||
|
|
@ -153,71 +142,5 @@ private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
|
|||
def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
|
||||
collectTacticNodes t |>.filter fun i => i.info.isSubstantive
|
||||
|
||||
@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
|
||||
def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
|
||||
let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
|
||||
| info@(.ofTacticInfo _) => info.isOriginal
|
||||
| _ => false
|
||||
let tactics := tacticInfoTrees.bind collectTactics
|
||||
tactics.mapM λ invocation => do
|
||||
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
|
||||
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
|
||||
let tactic ← invocation.ctx.runMetaM {} do
|
||||
let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
|
||||
return t.pretty
|
||||
let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
|
||||
return {
|
||||
goalBefore,
|
||||
goalAfter,
|
||||
tactic,
|
||||
usedConstants,
|
||||
}
|
||||
|
||||
structure InfoWithContext where
|
||||
info: Elab.Info
|
||||
context?: Option Elab.ContextInfo := .none
|
||||
|
||||
private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
|
||||
let infos := findAllInfo t none fun i => match i with
|
||||
| .ofTermInfo { expectedType?, expr, stx, .. } =>
|
||||
expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
|
||||
| .ofTacticInfo { stx, goalsBefore, .. } =>
|
||||
-- The `sorry` term is distinct from the `sorry` tactic
|
||||
let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
|
||||
isSorry ∧ !goalsBefore.isEmpty
|
||||
| _ => false
|
||||
infos.map fun (info, context?, _) => { info, context? }
|
||||
|
||||
-- NOTE: Plural deliberately not spelled "sorries"
|
||||
@[export pantograph_frontend_collect_sorrys_m]
|
||||
def collectSorrys (step: CompilationStep) : List InfoWithContext :=
|
||||
step.trees.bind collectSorrysInTree
|
||||
|
||||
|
||||
|
||||
/--
|
||||
Since we cannot directly merge `MetavarContext`s, we have to get creative. This
|
||||
function duplicates frozen mvars in term and tactic info nodes, and add them to
|
||||
the current `MetavarContext`.
|
||||
-/
|
||||
@[export pantograph_frontend_sorrys_to_goal_state]
|
||||
def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
|
||||
assert! !sorrys.isEmpty
|
||||
let goalsM := sorrys.mapM λ i => do
|
||||
match i.info with
|
||||
| .ofTermInfo termInfo => do
|
||||
let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
|
||||
return [mvarId]
|
||||
| .ofTacticInfo tacticInfo => do
|
||||
MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
|
||||
| _ => panic! "Invalid info"
|
||||
let goals := List.join (← goalsM.run {} |>.run' {})
|
||||
let root := match goals with
|
||||
| [] => panic! "No MVars generated"
|
||||
| [g] => g
|
||||
| _ => { name := .anonymous }
|
||||
GoalState.createFromMVars goals root
|
||||
|
||||
|
||||
|
||||
end Pantograph.Frontend
|
||||
end Pantograph.Compile
|
||||
|
|
@ -8,7 +8,6 @@ namespace Lean.FileMap
|
|||
/-- Extract the range of a `Syntax` expressed as lines and columns. -/
|
||||
-- Extracted from the private declaration `Lean.Elab.formatStxRange`,
|
||||
-- in `Lean.Elab.InfoTree.Main`.
|
||||
@[export pantograph_frontend_stx_range]
|
||||
protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position :=
|
||||
let pos := stx.getPos?.getD 0
|
||||
let endPos := stx.getTailPos?.getD pos
|
||||
|
|
@ -28,9 +27,7 @@ protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :
|
|||
end Lean.PersistentArray
|
||||
|
||||
|
||||
namespace Pantograph.Frontend
|
||||
|
||||
abbrev FrontendM := Elab.Frontend.FrontendM
|
||||
namespace Pantograph.Compile
|
||||
|
||||
structure CompilationStep where
|
||||
fileName : String
|
||||
|
|
@ -42,21 +39,12 @@ structure CompilationStep where
|
|||
msgs : List Message
|
||||
trees : List Elab.InfoTree
|
||||
|
||||
namespace CompilationStep
|
||||
|
||||
@[export pantograph_frontend_compilation_step_message_strings_m]
|
||||
def messageStrings (step: CompilationStep) : IO (Array String) := do
|
||||
List.toArray <$> step.msgs.mapM (·.toString)
|
||||
|
||||
end CompilationStep
|
||||
|
||||
|
||||
/--
|
||||
Process one command, returning a `CompilationStep` and
|
||||
`done : Bool`, indicating whether this was the last command.
|
||||
-/
|
||||
@[export pantograph_frontend_process_one_command_m]
|
||||
def processOneCommand: FrontendM (CompilationStep × Bool) := do
|
||||
def processOneCommand: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
|
||||
let s := (← get).commandState
|
||||
let before := s.env
|
||||
let done ← Elab.Frontend.processCommand
|
||||
|
|
@ -69,52 +57,30 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
|
|||
let ⟨_, fileName, fileMap⟩ := (← read).inputCtx
|
||||
return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
|
||||
|
||||
partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
|
||||
partial def processFile : Elab.Frontend.FrontendM (List CompilationStep) := do
|
||||
let (cmd, done) ← processOneCommand
|
||||
if done then
|
||||
if cmd.src.isEmpty then
|
||||
return []
|
||||
else
|
||||
return [← f cmd]
|
||||
return [cmd]
|
||||
else
|
||||
return (← f cmd) :: (← mapCompilationSteps f)
|
||||
return cmd :: (← processFile)
|
||||
|
||||
|
||||
@[export pantograph_frontend_find_source_path_m]
|
||||
def findSourcePath (module : Name) : IO System.FilePath := do
|
||||
return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
|
||||
|
||||
/--
|
||||
Use with
|
||||
```lean
|
||||
let m: FrontendM α := ...
|
||||
let (context, state) ← createContextStateFromFile ...
|
||||
m.run context |>.run' state
|
||||
```
|
||||
-/
|
||||
@[export pantograph_frontend_create_context_state_from_file_m]
|
||||
def createContextStateFromFile
|
||||
(file : String) -- Content of the file
|
||||
(fileName : String := "<anonymous>")
|
||||
(env? : Option Lean.Environment := .none) -- If set to true, assume there's no header.
|
||||
(opts : Options := {})
|
||||
: IO (Elab.Frontend.Context × Elab.Frontend.State) := unsafe do
|
||||
--let file ← IO.FS.readFile (← findSourcePath module)
|
||||
let inputCtx := Parser.mkInputContext file fileName
|
||||
def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe do
|
||||
let file ← IO.FS.readFile (← findSourcePath module)
|
||||
let inputCtx := Parser.mkInputContext file module.toString
|
||||
|
||||
let (env, parserState, messages) ← match env? with
|
||||
| .some env => pure (env, {}, .empty)
|
||||
| .none =>
|
||||
let (header, parserState, messages) ← Parser.parseHeader inputCtx
|
||||
let (env, messages) ← Elab.processHeader header opts messages inputCtx
|
||||
pure (env, parserState, messages)
|
||||
let (header, parserState, messages) ← Parser.parseHeader inputCtx
|
||||
let (env, messages) ← Elab.processHeader header opts messages inputCtx
|
||||
let commandState := Elab.Command.mkState env messages opts
|
||||
let context: Elab.Frontend.Context := { inputCtx }
|
||||
let state: Elab.Frontend.State := {
|
||||
processFile.run { inputCtx }
|
||||
|>.run' {
|
||||
commandState := { commandState with infoState.enabled := true },
|
||||
parserState,
|
||||
cmdPos := parserState.pos
|
||||
}
|
||||
return (context, state)
|
||||
|
||||
end Pantograph.Frontend
|
||||
|
||||
end Pantograph.Compile
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Compile
|
||||
|
||||
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
|
||||
return Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
end Pantograph.Compile
|
||||
|
|
@ -0,0 +1,96 @@
|
|||
/- structures for FFI based interface -/
|
||||
import Lean
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Expr
|
||||
import Pantograph.Protocol
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
namespace Condensed
|
||||
|
||||
-- Mirrors Lean's LocalDecl
|
||||
structure LocalDecl where
|
||||
-- Default value is for testing
|
||||
fvarId: FVarId := { name := .anonymous }
|
||||
userName: Name
|
||||
|
||||
-- Normalized expression
|
||||
type : Expr
|
||||
value? : Option Expr := .none
|
||||
|
||||
structure Goal where
|
||||
mvarId: MVarId := { name := .anonymous }
|
||||
userName: Name := .anonymous
|
||||
context: Array LocalDecl
|
||||
target: Expr
|
||||
|
||||
@[export pantograph_goal_is_lhs]
|
||||
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
|
||||
|
||||
-- Functions for creating contexts and states
|
||||
@[export pantograph_elab_context]
|
||||
def elabContext: Elab.Term.Context := {
|
||||
errToSorry := false
|
||||
}
|
||||
|
||||
end Condensed
|
||||
|
||||
-- Get the list of visible (by default) free variables from a goal
|
||||
@[export pantograph_visible_fvars_of_mvar]
|
||||
protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
|
||||
let mvarDecl ← mctx.findDecl? mvarId
|
||||
let lctx := mvarDecl.lctx
|
||||
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
|
||||
| some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
|
||||
| none => r
|
||||
|
||||
@[export pantograph_to_condensed_goal_m]
|
||||
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
|
||||
let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions)
|
||||
let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let type ← instantiate type
|
||||
return { fvarId, userName, type }
|
||||
| .ldecl _ fvarId userName type value _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value ← instantiate value
|
||||
return { fvarId, userName, type, value? := .some value }
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let var ← ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
mvarId,
|
||||
userName := mvarDecl.userName,
|
||||
context := vars.reverse.toArray,
|
||||
target := ← instantiate mvarDecl.type
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
|
||||
@[export pantograph_goal_state_to_condensed_m]
|
||||
protected def GoalState.toCondensed (state: GoalState):
|
||||
CoreM (Array Condensed.Goal):= do
|
||||
let metaM := do
|
||||
let goals := state.goals.toArray
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some _ =>
|
||||
let serializedGoal ← toCondensedGoal goal
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
metaM.run' (s := state.savedState.term.meta.meta)
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -1,562 +0,0 @@
|
|||
/-
|
||||
This file handles "Delation": The conversion of Kernel view into Search view.
|
||||
-/
|
||||
import Lean
|
||||
import Std.Data.HashMap
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
|
||||
open Lean
|
||||
|
||||
-- Symbol processing functions --
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
structure ProjectionApplication where
|
||||
projector: Name
|
||||
numParams: Nat
|
||||
inner: Expr
|
||||
|
||||
@[export pantograph_expr_proj_to_app]
|
||||
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
|
||||
let (typeName, idx, inner) := match e with
|
||||
| .proj typeName idx inner => (typeName, idx, inner)
|
||||
| _ => panic! "Argument must be proj"
|
||||
let ctor := getStructureCtor env typeName
|
||||
let fieldName := getStructureFields env typeName |>.get! idx
|
||||
let projector := getProjFnForField? env typeName fieldName |>.get!
|
||||
{
|
||||
projector,
|
||||
numParams := ctor.numParams,
|
||||
inner,
|
||||
}
|
||||
|
||||
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
|
||||
|
||||
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
|
||||
@[export pantograph_unfold_aux_lemmas]
|
||||
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
|
||||
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
|
||||
|
||||
/--
|
||||
Force the instantiation of delayed metavariables even if they cannot be fully
|
||||
instantiated. This is used during resumption to provide diagnostic data about
|
||||
the current goal.
|
||||
|
||||
Since Lean 4 does not have an `Expr` constructor corresponding to delayed
|
||||
metavariables, any delayed metavariables must be recursively handled by this
|
||||
function to ensure that nested delayed metavariables can be properly processed.
|
||||
The caveat is this recursive call will lead to infinite recursion if a loop
|
||||
between metavariable assignment exists.
|
||||
|
||||
This function ensures any metavariable in the result is either
|
||||
1. Delayed assigned with its pending mvar not assigned in any form
|
||||
2. Not assigned (delay or not)
|
||||
-/
|
||||
partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
|
||||
--let padding := String.join $ List.replicate level "│ "
|
||||
--IO.println s!"{padding}Starting {toString eOrig}"
|
||||
let mut result ← Meta.transform (← instantiateMVars eOrig)
|
||||
(pre := fun e => e.withApp fun f args => do
|
||||
let .mvar mvarId := f | return .continue
|
||||
--IO.println s!"{padding}├V {e}"
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
|
||||
-- This is critical to maintaining the interdependency of metavariables.
|
||||
-- Without setting `.syntheticOpaque`, Lean's metavariable elimination
|
||||
-- system will not make the necessary delayed assigned mvars in case of
|
||||
-- nested mvars.
|
||||
mvarId.setKind .syntheticOpaque
|
||||
|
||||
mvarId.withContext do
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
|
||||
let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
|
||||
| .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
|
||||
| .none => acc) []
|
||||
panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
|
||||
|
||||
if let .some assign ← getExprMVarAssignment? mvarId then
|
||||
--IO.println s!"{padding}├A ?{mvarId.name}"
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
return .visit (mkAppN assign args)
|
||||
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
|
||||
--let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
|
||||
--IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
|
||||
|
||||
if args.size < fvars.size then
|
||||
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments End"
|
||||
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
|
||||
--IO.println s!"{padding}├T1"
|
||||
let result := mkAppN f args
|
||||
return .done result
|
||||
|
||||
let pending ← mvarIdPending.withContext do
|
||||
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
|
||||
--IO.println s!"{padding}├Pre: {inner}"
|
||||
pure <| (← inner.abstractM fvars).instantiateRev args
|
||||
|
||||
-- Tail arguments
|
||||
let result := mkAppRange pending fvars.size args.size args
|
||||
--IO.println s!"{padding}├MD {result}"
|
||||
return .done result
|
||||
else
|
||||
assert! !(← mvarId.isAssigned)
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments End"
|
||||
|
||||
--IO.println s!"{padding}├M ?{mvarId.name}"
|
||||
return .done (mkAppN f args))
|
||||
--IO.println s!"{padding}└Result {result}"
|
||||
return result
|
||||
where
|
||||
self e := instantiateDelayedMVars e --(level := level + 1)
|
||||
|
||||
/--
|
||||
Convert an expression to an equiavlent form with
|
||||
1. No nested delayed assigned mvars
|
||||
2. No aux lemmas
|
||||
3. No assigned mvars
|
||||
-/
|
||||
@[export pantograph_instantiate_all_m]
|
||||
def instantiateAll (e: Expr): MetaM Expr := do
|
||||
let e ← instantiateDelayedMVars e
|
||||
let e ← unfoldAuxLemmas e
|
||||
return e
|
||||
|
||||
structure DelayedMVarInvocation where
|
||||
mvarIdPending: MVarId
|
||||
args: Array (FVarId × (Option Expr))
|
||||
-- Extra arguments applied to the result of this substitution
|
||||
tail: Array Expr
|
||||
|
||||
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
|
||||
@[export pantograph_to_delayed_mvar_invocation_m]
|
||||
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
|
||||
let .mvar mvarId := e.getAppFn | return .none
|
||||
let .some decl ← getDelayedMVarAssignment? mvarId | return .none
|
||||
let mvarIdPending := decl.mvarIdPending
|
||||
let mvarDecl ← mvarIdPending.getDecl
|
||||
-- Print the function application e. See Lean's `withOverApp`
|
||||
let args := e.getAppArgs
|
||||
|
||||
assert! args.size ≥ decl.fvars.size
|
||||
assert! !(← mvarIdPending.isAssigned)
|
||||
assert! !(← mvarIdPending.isDelayedAssigned)
|
||||
let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
|
||||
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
|
||||
let fvarId := localDecl.fvarId
|
||||
let a := fvarArgMap[fvarId]?
|
||||
return acc ++ [(fvarId, a)]
|
||||
|
||||
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
|
||||
|
||||
return .some {
|
||||
mvarIdPending,
|
||||
args := subst.toArray,
|
||||
tail := args.toList.drop decl.fvars.size |>.toArray,
|
||||
}
|
||||
|
||||
-- Condensed representation
|
||||
|
||||
namespace Condensed
|
||||
|
||||
-- Mirrors Lean's LocalDecl
|
||||
structure LocalDecl where
|
||||
-- Default value is for testing
|
||||
fvarId: FVarId := { name := .anonymous }
|
||||
userName: Name
|
||||
|
||||
-- Normalized expression
|
||||
type : Expr
|
||||
value? : Option Expr := .none
|
||||
|
||||
structure Goal where
|
||||
mvarId: MVarId := { name := .anonymous }
|
||||
userName: Name := .anonymous
|
||||
context: Array LocalDecl
|
||||
target: Expr
|
||||
|
||||
@[export pantograph_goal_is_lhs]
|
||||
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
|
||||
|
||||
end Condensed
|
||||
|
||||
-- Get the list of visible (by default) free variables from a goal
|
||||
@[export pantograph_visible_fvars_of_mvar]
|
||||
protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
|
||||
let mvarDecl ← mctx.findDecl? mvarId
|
||||
let lctx := mvarDecl.lctx
|
||||
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
|
||||
| some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
|
||||
| none => r
|
||||
|
||||
@[export pantograph_to_condensed_goal_m]
|
||||
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
|
||||
let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions)
|
||||
let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let type ← instantiate type
|
||||
return { fvarId, userName, type }
|
||||
| .ldecl _ fvarId userName type value _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value ← instantiate value
|
||||
return { fvarId, userName, type, value? := .some value }
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let var ← ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
mvarId,
|
||||
userName := mvarDecl.userName,
|
||||
context := vars.reverse.toArray,
|
||||
target := ← instantiate mvarDecl.type
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
|
||||
@[export pantograph_goal_state_to_condensed_m]
|
||||
protected def GoalState.toCondensed (state: GoalState):
|
||||
CoreM (Array Condensed.Goal):= do
|
||||
let metaM := do
|
||||
let goals := state.goals.toArray
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some _ =>
|
||||
let serializedGoal ← toCondensedGoal goal
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
metaM.run' (s := state.savedState.term.meta.meta)
|
||||
|
||||
def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
|
||||
Meta.forallTelescope expr fun arr body => do
|
||||
let binders ← arr.mapM fun fvar => do
|
||||
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
|
||||
return { binders, target := toString (← Meta.ppExpr body) }
|
||||
|
||||
def serializeName (name: Name) (sanitize: Bool := true): String :=
|
||||
let internal := name.isInaccessibleUserName || name.hasMacroScopes
|
||||
if sanitize && internal then "_"
|
||||
else toString name |> addQuotes
|
||||
where
|
||||
addQuotes (n: String) :=
|
||||
let quote := "\""
|
||||
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
|
||||
|
||||
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
|
||||
partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
|
||||
let k := level.getOffset
|
||||
let u := level.getLevelOffset
|
||||
let u_str := match u with
|
||||
| .zero => "0"
|
||||
| .succ _ => panic! "getLevelOffset should not return .succ"
|
||||
| .max v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:max {v} {w})"
|
||||
| .imax v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:imax {v} {w})"
|
||||
| .param name =>
|
||||
let name := serializeName name sanitize
|
||||
s!"{name}"
|
||||
| .mvar id =>
|
||||
let name := serializeName id.name sanitize
|
||||
s!"(:mv {name})"
|
||||
match k, u with
|
||||
| 0, _ => u_str
|
||||
| _, .zero => s!"{k}"
|
||||
| _, _ => s!"(+ {u_str} {k})"
|
||||
|
||||
|
||||
/--
|
||||
Completely serializes an expression tree. Json not used due to compactness
|
||||
|
||||
A `_` symbol in the AST indicates automatic deductions not present in the original expression.
|
||||
-/
|
||||
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
|
||||
self expr
|
||||
where
|
||||
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
|
||||
let .some invocation ← toDelayedMVarInvocation e | return .none
|
||||
let callee ← self $ .mvar invocation.mvarIdPending
|
||||
let sites ← invocation.args.mapM (λ (fvarId, arg) => do
|
||||
let arg := match arg with
|
||||
| .some arg => arg
|
||||
| .none => .fvar fvarId
|
||||
self arg
|
||||
)
|
||||
let tailArgs ← invocation.tail.mapM self
|
||||
|
||||
let sites := " ".intercalate sites.toList
|
||||
let result := if tailArgs.isEmpty then
|
||||
s!"(:subst {callee} {sites})"
|
||||
else
|
||||
let tailArgs := " ".intercalate tailArgs.toList
|
||||
s!"((:subst {callee} {sites}) {tailArgs})"
|
||||
return .some result
|
||||
|
||||
self (e: Expr): MetaM String := do
|
||||
if let .some result ← delayedMVarToSexp e then
|
||||
return result
|
||||
match e with
|
||||
| .bvar deBruijnIndex =>
|
||||
-- This is very common so the index alone is shown. Literals are handled below.
|
||||
-- The raw de Bruijn index should never appear in an unbound setting. In
|
||||
-- Lean these are handled using a `#` prefix.
|
||||
pure s!"{deBruijnIndex}"
|
||||
| .fvar fvarId =>
|
||||
let name := ofName fvarId.name
|
||||
pure s!"(:fv {name})"
|
||||
| .mvar mvarId => do
|
||||
let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
|
||||
let name := ofName mvarId.name
|
||||
pure s!"(:{pref} {name})"
|
||||
| .sort level =>
|
||||
let level := serializeSortLevel level sanitize
|
||||
pure s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
-- The universe level of the const expression is elided since it should be
|
||||
-- inferrable from surrounding expression
|
||||
pure s!"(:c {declName})"
|
||||
| .app _ _ => do
|
||||
let fn' ← self e.getAppFn
|
||||
let args := (← e.getAppArgs.mapM self) |>.toList
|
||||
let args := " ".intercalate args
|
||||
pure s!"({fn'} {args})"
|
||||
| .lam binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .forallE binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .letE name type value body _ => do
|
||||
-- Dependent boolean flag diacarded
|
||||
let name' := serializeName name
|
||||
let type' ← self type
|
||||
let value' ← self value
|
||||
let body' ← self body
|
||||
pure s!"(:let {name'} {type'} {value'} {body'})"
|
||||
| .lit v =>
|
||||
-- To not burden the downstream parser who needs to handle this, the literal
|
||||
-- is wrapped in a :lit sexp.
|
||||
let v' := match v with
|
||||
| .natVal val => toString val
|
||||
| .strVal val => s!"\"{val}\""
|
||||
pure s!"(:lit {v'})"
|
||||
| .mdata _ inner =>
|
||||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
-- It may become necessary to incorporate the metadata.
|
||||
self inner
|
||||
| .proj _ _ _ => do
|
||||
let env ← getEnv
|
||||
let projApp := exprProjToApp env e
|
||||
let autos := String.intercalate " " (List.replicate projApp.numParams "_")
|
||||
let inner ← self projApp.inner
|
||||
pure s!"((:c {projApp.projector}) {autos} {inner})"
|
||||
-- Elides all unhygenic names
|
||||
binderInfoSexp : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
| .implicit => " :implicit"
|
||||
| .strictImplicit => " :strictImplicit"
|
||||
| .instImplicit => " :instImplicit"
|
||||
ofName (name: Name) := serializeName name sanitize
|
||||
|
||||
def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
|
||||
let pp?: Option String ← match options.printExprPretty with
|
||||
| true => pure $ .some $ toString $ ← Meta.ppExpr e
|
||||
| false => pure $ .none
|
||||
let sexp?: Option String ← match options.printExprAST with
|
||||
| true => pure $ .some $ ← serializeExpressionSexp e
|
||||
| false => pure $ .none
|
||||
let dependentMVars? ← match options.printDependentMVars with
|
||||
| true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
|
||||
| false => pure $ .none
|
||||
return {
|
||||
pp?,
|
||||
sexp?
|
||||
dependentMVars?,
|
||||
}
|
||||
|
||||
|
||||
/-- Adapted from ppGoal -/
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
|
||||
: MetaM Protocol.Goal := do
|
||||
-- Options for printing; See Meta.ppGoal for details
|
||||
let showLetValues := true
|
||||
let ppAuxDecls := options.printAuxDecls
|
||||
let ppImplDetailHyps := options.printImplementationDetailHyps
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName _ _ _ =>
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
}
|
||||
| .ldecl _ fvarId userName type val _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value? ← if showLetValues then
|
||||
let val ← instantiate val
|
||||
pure $ .some (← serializeExpression options val)
|
||||
else
|
||||
pure $ .none
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
value? := value?
|
||||
}
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let nameOnly := options.noRepeat && (parentDecl?.map
|
||||
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
|
||||
let var ← match nameOnly with
|
||||
| true => ppVarNameOnly localDecl
|
||||
| false => ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
name := ofName goal.name,
|
||||
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
|
||||
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
|
||||
target := (← serializeExpression options (← instantiate mvarDecl.type)),
|
||||
vars := vars.reverse.toArray
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
ofName (n: Name) := serializeName n (sanitize := false)
|
||||
|
||||
protected def GoalState.serializeGoals
|
||||
(state: GoalState)
|
||||
(parent: Option GoalState := .none)
|
||||
(options: @&Protocol.Options := {}):
|
||||
MetaM (Array Protocol.Goal):= do
|
||||
state.restoreMetaM
|
||||
let goals := state.goals.toArray
|
||||
let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some mvarDecl =>
|
||||
let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
|
||||
/-- Print the metavariables in a readable format -/
|
||||
@[export pantograph_goal_state_diag_m]
|
||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
|
||||
let metaM: MetaM String := do
|
||||
goalState.restoreMetaM
|
||||
let savedState := goalState.savedState
|
||||
let goals := savedState.tactic.goals
|
||||
let mctx ← getMCtx
|
||||
let root := goalState.root
|
||||
-- Print the root
|
||||
let result: String ← match mctx.decls.find? root with
|
||||
| .some decl => printMVar ">" root decl
|
||||
| .none => pure s!">{root.name}: ??"
|
||||
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
|
||||
match mctx.decls.find? mvarId with
|
||||
| .some decl => printMVar "⊢" mvarId decl
|
||||
| .none => pure s!"⊢{mvarId.name}: ??"
|
||||
)
|
||||
let goals := goals.toSSet
|
||||
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
|
||||
!(goals.contains mvarId || mvarId == root) && options.printAll)
|
||||
|>.mapM (fun (mvarId, decl) => do
|
||||
let pref := if parentHasMVar mvarId then " " else "~"
|
||||
printMVar pref mvarId decl
|
||||
)
|
||||
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
||||
metaM.run' {}
|
||||
where
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
||||
let resultFVars: List String ←
|
||||
if options.printContext then
|
||||
decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
|
||||
do pure $ (← printFVar fvarId decl) ++ "\n")
|
||||
else
|
||||
pure []
|
||||
let type ← if options.instantiate
|
||||
then instantiateAll decl.type
|
||||
else pure $ decl.type
|
||||
let type_sexp ← if options.printSexp then
|
||||
let sexp ← serializeExpressionSexp type (sanitize := false)
|
||||
pure <| " " ++ sexp
|
||||
else
|
||||
pure ""
|
||||
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
|
||||
let resultValue: String ←
|
||||
if options.printValue then
|
||||
if let .some value ← getExprMVarAssignment? mvarId then
|
||||
let value ← if options.instantiate
|
||||
then instantiateAll value
|
||||
else pure $ value
|
||||
pure s!"\n := {← Meta.ppExpr value}"
|
||||
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
|
||||
pure s!"\n ::= {mvarIdPending.name}"
|
||||
else
|
||||
pure ""
|
||||
else
|
||||
pure ""
|
||||
pure $ (String.join resultFVars) ++ resultMain ++ resultValue
|
||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
|
||||
pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||
userNameToString : Name → String
|
||||
| .anonymous => ""
|
||||
| other => s!"[{other}]"
|
||||
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -1,40 +0,0 @@
|
|||
import Lean
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
-- Functions for creating contexts and states
|
||||
@[export pantograph_default_elab_context]
|
||||
def defaultElabContext: Elab.Term.Context := {
|
||||
errToSorry := false
|
||||
}
|
||||
|
||||
/-- Read syntax object from string -/
|
||||
def parseTerm (env: Environment) (s: String): Except String Syntax :=
|
||||
Parser.runParserCategory
|
||||
(env := env)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
|
||||
return Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
/-- Parse a syntax object. May generate additional metavariables! -/
|
||||
def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabType syn
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -1,9 +1,6 @@
|
|||
import Pantograph.Delate
|
||||
import Pantograph.Elab
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Serial
|
||||
import Lean.Environment
|
||||
import Lean.Replay
|
||||
import Lean
|
||||
|
||||
open Lean
|
||||
open Pantograph
|
||||
|
|
@ -13,12 +10,16 @@ namespace Pantograph.Environment
|
|||
@[export pantograph_is_name_internal]
|
||||
def isNameInternal (n: Name): Bool :=
|
||||
-- Returns true if the name is an implementation detail which should not be shown to the user.
|
||||
n.isAuxLemma ∨ n.hasMacroScopes
|
||||
isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
|
||||
where
|
||||
isLeanSymbol (name: Name): Bool := match name.getRoot with
|
||||
| .str _ name => name == "Lean"
|
||||
| _ => true
|
||||
|
||||
/-- Catalog all the non-internal and safe names -/
|
||||
@[export pantograph_environment_catalog]
|
||||
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
|
||||
match isNameInternal name with
|
||||
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info =>
|
||||
match isNameInternal name || info.isUnsafe with
|
||||
| false => acc.push name
|
||||
| true => acc)
|
||||
|
||||
|
|
@ -27,6 +28,14 @@ def module_of_name (env: Environment) (name: Name): Option Name := do
|
|||
let moduleId ← env.getModuleIdxFor? name
|
||||
return env.allImportedModuleNames.get! moduleId.toNat
|
||||
|
||||
@[export pantograph_constant_info_is_unsafe_or_partial]
|
||||
def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
|
||||
|
||||
@[export pantograph_constant_info_type]
|
||||
def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type
|
||||
@[export pantograph_constant_info_value]
|
||||
def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas
|
||||
|
||||
def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
|
||||
let pref := match info with
|
||||
| .axiomInfo _ => "a"
|
||||
|
|
|
|||
|
|
@ -0,0 +1,160 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
structure ProjectionApplication where
|
||||
projector: Name
|
||||
numParams: Nat
|
||||
inner: Expr
|
||||
|
||||
@[export pantograph_expr_proj_to_app]
|
||||
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
|
||||
let (typeName, idx, inner) := match e with
|
||||
| .proj typeName idx inner => (typeName, idx, inner)
|
||||
| _ => panic! "Argument must be proj"
|
||||
let ctor := getStructureCtor env typeName
|
||||
let fieldName := getStructureFields env typeName |>.get! idx
|
||||
let projector := getProjFnForField? env typeName fieldName |>.get!
|
||||
{
|
||||
projector,
|
||||
numParams := ctor.numParams,
|
||||
inner,
|
||||
}
|
||||
|
||||
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
|
||||
|
||||
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
|
||||
@[export pantograph_unfold_aux_lemmas]
|
||||
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
|
||||
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
|
||||
|
||||
/--
|
||||
Force the instantiation of delayed metavariables even if they cannot be fully
|
||||
instantiated. This is used during resumption to provide diagnostic data about
|
||||
the current goal.
|
||||
|
||||
Since Lean 4 does not have an `Expr` constructor corresponding to delayed
|
||||
metavariables, any delayed metavariables must be recursively handled by this
|
||||
function to ensure that nested delayed metavariables can be properly processed.
|
||||
The caveat is this recursive call will lead to infinite recursion if a loop
|
||||
between metavariable assignment exists.
|
||||
|
||||
This function ensures any metavariable in the result is either
|
||||
1. Delayed assigned with its pending mvar not assigned in any form
|
||||
2. Not assigned (delay or not)
|
||||
-/
|
||||
partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
|
||||
--let padding := String.join $ List.replicate level "│ "
|
||||
--IO.println s!"{padding}Starting {toString eOrig}"
|
||||
let mut result ← Meta.transform (← instantiateMVars eOrig)
|
||||
(pre := fun e => e.withApp fun f args => do
|
||||
let .mvar mvarId := f | return .continue
|
||||
--IO.println s!"{padding}├V {e}"
|
||||
let mvarDecl ← mvarId.getDecl
|
||||
|
||||
-- This is critical to maintaining the interdependency of metavariables.
|
||||
-- Without setting `.syntheticOpaque`, Lean's metavariable elimination
|
||||
-- system will not make the necessary delayed assigned mvars in case of
|
||||
-- nested mvars.
|
||||
mvarId.setKind .syntheticOpaque
|
||||
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
|
||||
let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
|
||||
| .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
|
||||
| .none => acc) []
|
||||
panic! s!"Local context variable violation: {violations}"
|
||||
|
||||
if let .some assign ← getExprMVarAssignment? mvarId then
|
||||
--IO.println s!"{padding}├A ?{mvarId.name}"
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
return .visit (mkAppN assign args)
|
||||
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
|
||||
--let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
|
||||
--IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
|
||||
|
||||
if args.size < fvars.size then
|
||||
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
--IO.println s!"{padding}├── Arguments End"
|
||||
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
|
||||
--IO.println s!"{padding}├T1"
|
||||
let result := mkAppN f args
|
||||
return .done result
|
||||
|
||||
let pending ← mvarIdPending.withContext do
|
||||
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
|
||||
--IO.println s!"{padding}├Pre: {inner}"
|
||||
pure <| (← inner.abstractM fvars).instantiateRev args
|
||||
|
||||
-- Tail arguments
|
||||
let result := mkAppRange pending fvars.size args.size args
|
||||
--IO.println s!"{padding}├MD {result}"
|
||||
return .done result
|
||||
else
|
||||
assert! !(← mvarId.isAssigned)
|
||||
assert! !(← mvarId.isDelayedAssigned)
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments Begin"
|
||||
let args ← args.mapM self
|
||||
--if !args.isEmpty then
|
||||
-- IO.println s!"{padding}├── Arguments End"
|
||||
|
||||
--IO.println s!"{padding}├M ?{mvarId.name}"
|
||||
return .done (mkAppN f args))
|
||||
--IO.println s!"{padding}└Result {result}"
|
||||
return result
|
||||
where
|
||||
self e := instantiateDelayedMVars e --(level := level + 1)
|
||||
|
||||
/--
|
||||
Convert an expression to an equiavlent form with
|
||||
1. No nested delayed assigned mvars
|
||||
2. No aux lemmas
|
||||
3. No assigned mvars
|
||||
-/
|
||||
@[export pantograph_instantiate_all_m]
|
||||
def instantiateAll (e: Expr): MetaM Expr := do
|
||||
let e ← instantiateDelayedMVars e
|
||||
let e ← unfoldAuxLemmas e
|
||||
return e
|
||||
|
||||
structure DelayedMVarInvocation where
|
||||
mvarIdPending: MVarId
|
||||
args: Array (FVarId × (Option Expr))
|
||||
-- Extra arguments applied to the result of this substitution
|
||||
tail: Array Expr
|
||||
|
||||
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
|
||||
@[export pantograph_to_delayed_mvar_invocation_m]
|
||||
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
|
||||
let .mvar mvarId := e.getAppFn | return .none
|
||||
let .some decl ← getDelayedMVarAssignment? mvarId | return .none
|
||||
let mvarIdPending := decl.mvarIdPending
|
||||
let mvarDecl ← mvarIdPending.getDecl
|
||||
-- Print the function application e. See Lean's `withOverApp`
|
||||
let args := e.getAppArgs
|
||||
|
||||
assert! args.size ≥ decl.fvars.size
|
||||
assert! !(← mvarIdPending.isAssigned)
|
||||
assert! !(← mvarIdPending.isDelayedAssigned)
|
||||
let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
|
||||
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
|
||||
let fvarId := localDecl.fvarId
|
||||
let a := fvarArgMap.find? fvarId
|
||||
return acc ++ [(fvarId, a)]
|
||||
|
||||
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
|
||||
|
||||
return .some {
|
||||
mvarIdPending,
|
||||
args := subst.toArray,
|
||||
tail := args.toList.drop decl.fvars.size |>.toArray,
|
||||
}
|
||||
|
||||
end Pantograph
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
/- Adapted from lean-training-data by semorrison -/
|
||||
import Pantograph.Frontend.Basic
|
||||
import Pantograph.Frontend.Elab
|
||||
import Pantograph.Frontend.MetaTranslate
|
||||
|
|
@ -1,164 +0,0 @@
|
|||
import Lean.Meta
|
||||
import Std.Data.HashMap
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Frontend
|
||||
|
||||
namespace MetaTranslate
|
||||
|
||||
structure Context where
|
||||
sourceMCtx : MetavarContext := {}
|
||||
sourceLCtx : LocalContext := {}
|
||||
|
||||
abbrev FVarMap := Std.HashMap FVarId FVarId
|
||||
|
||||
structure State where
|
||||
-- Stores mapping from old to new mvar/fvars
|
||||
mvarMap: Std.HashMap MVarId MVarId := {}
|
||||
fvarMap: Std.HashMap FVarId FVarId := {}
|
||||
|
||||
/-
|
||||
Monadic state for translating a frozen meta state. The underlying `MetaM`
|
||||
operates in the "target" context and state.
|
||||
-/
|
||||
abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM
|
||||
|
||||
def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx
|
||||
def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx
|
||||
def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do
|
||||
modifyGet λ state => ((), { state with fvarMap := state.fvarMap.insert src dst })
|
||||
def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do
|
||||
modifyGet λ state => ((), { state with mvarMap := state.mvarMap.insert src dst })
|
||||
|
||||
def saveFVarMap : MetaTranslateM FVarMap := do
|
||||
return (← get).fvarMap
|
||||
def restoreFVarMap (map: FVarMap) : MetaTranslateM Unit := do
|
||||
modifyGet λ state => ((), { state with fvarMap := map })
|
||||
def resetFVarMap : MetaTranslateM Unit := do
|
||||
modifyGet λ state => ((), { state with fvarMap := {} })
|
||||
|
||||
mutual
|
||||
private partial def translateLevel (srcLevel: Level) : MetaTranslateM Level := do
|
||||
let sourceMCtx ← getSourceMCtx
|
||||
let (_, level) := instantiateLevelMVarsImp sourceMCtx srcLevel
|
||||
match level with
|
||||
| .zero => return .zero
|
||||
| .succ inner => do
|
||||
let inner' ← translateLevel inner
|
||||
return .succ inner'
|
||||
| .max l1 l2 => do
|
||||
let l1' ← translateLevel l1
|
||||
let l2' ← translateLevel l2
|
||||
return .max l1' l2'
|
||||
| .imax l1 l2 => do
|
||||
let l1' ← translateLevel l1
|
||||
let l2' ← translateLevel l2
|
||||
return .imax l1' l2'
|
||||
| .param p => return .param p
|
||||
| .mvar _ =>
|
||||
Meta.mkFreshLevelMVar
|
||||
private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
|
||||
let sourceMCtx ← getSourceMCtx
|
||||
-- We want to create as few mvars as possible
|
||||
let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
|
||||
--IO.println s!"Transform src: {srcExpr}"
|
||||
let result ← Core.transform srcExpr λ e => do
|
||||
let state ← get
|
||||
match e with
|
||||
| .fvar fvarId =>
|
||||
let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
|
||||
assert! (← getLCtx).contains fvarId'
|
||||
return .done $ .fvar fvarId'
|
||||
| .mvar mvarId => do
|
||||
-- Must not be assigned
|
||||
assert! !(sourceMCtx.eAssignment.contains mvarId)
|
||||
match state.mvarMap[mvarId]? with
|
||||
| .some mvarId' => do
|
||||
return .done $ .mvar mvarId'
|
||||
| .none => do
|
||||
-- Entering another LCtx, must save the current one
|
||||
let fvarMap ← saveFVarMap
|
||||
let mvarId' ← translateMVarId mvarId
|
||||
restoreFVarMap fvarMap
|
||||
return .done $ .mvar mvarId'
|
||||
| .sort level => do
|
||||
let level' ← translateLevel level
|
||||
return .done $ .sort level'
|
||||
| _ => return .continue
|
||||
Meta.check result
|
||||
return result
|
||||
|
||||
partial def translateLocalInstance (srcInstance: LocalInstance) : MetaTranslateM LocalInstance := do
|
||||
return {
|
||||
className := srcInstance.className,
|
||||
fvar := ← translateExpr srcInstance.fvar
|
||||
}
|
||||
partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
|
||||
let fvarId ← mkFreshFVarId
|
||||
addTranslatedFVar srcLocalDecl.fvarId fvarId
|
||||
match srcLocalDecl with
|
||||
| .cdecl index _ userName type bi kind => do
|
||||
--IO.println s!"[CD] {userName} {toString type}"
|
||||
return .cdecl index fvarId userName (← translateExpr type) bi kind
|
||||
| .ldecl index _ userName type value nonDep kind => do
|
||||
--IO.println s!"[LD] {toString type} := {toString value}"
|
||||
return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
|
||||
|
||||
partial def translateLCtx : MetaTranslateM LocalContext := do
|
||||
resetFVarMap
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
assert! lctx.isEmpty
|
||||
(← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
|
||||
let localDecl ← Meta.withLCtx lctx #[] do
|
||||
translateLocalDecl srcLocalDecl
|
||||
pure $ lctx.addDecl localDecl
|
||||
) lctx
|
||||
|
||||
partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
|
||||
if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
|
||||
return mvarId'
|
||||
let mvarId' ← Meta.withLCtx .empty #[] do
|
||||
let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
|
||||
withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
|
||||
let lctx' ← translateLCtx
|
||||
let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
|
||||
Meta.withLCtx lctx' localInstances' do
|
||||
let target' ← translateExpr srcDecl.type
|
||||
let mvar' ← Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
|
||||
let mvarId' := mvar'.mvarId!
|
||||
if let .some { fvars, mvarIdPending }:= (← getSourceMCtx).getDelayedMVarAssignmentExp srcMVarId then
|
||||
-- Map the fvars in the pending context.
|
||||
let mvarIdPending' ← translateMVarId mvarIdPending
|
||||
let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
|
||||
assignDelayedMVar mvarId' fvars' mvarIdPending'
|
||||
pure mvarId'
|
||||
addTranslatedMVar srcMVarId mvarId'
|
||||
return mvarId'
|
||||
end
|
||||
|
||||
def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)
|
||||
: MetaTranslateM MVarId := do
|
||||
withTheReader Context (λ ctx => { ctx with
|
||||
sourceMCtx := context?.map (·.mctx) |>.getD {},
|
||||
sourceLCtx := termInfo.lctx,
|
||||
}) do
|
||||
let type := termInfo.expectedType?.get!
|
||||
let lctx' ← translateLCtx
|
||||
let mvar ← Meta.withLCtx lctx' #[] do
|
||||
let type' ← translateExpr type
|
||||
Meta.mkFreshExprSyntheticOpaqueMVar type'
|
||||
return mvar.mvarId!
|
||||
|
||||
|
||||
def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo)
|
||||
: MetaTranslateM (List MVarId) := do
|
||||
withTheReader Context (λ ctx => { ctx with sourceMCtx := tacticInfo.mctxBefore }) do
|
||||
tacticInfo.goalsBefore.mapM translateMVarId
|
||||
|
||||
|
||||
end MetaTranslate
|
||||
|
||||
export MetaTranslate (MetaTranslateM)
|
||||
|
||||
end Pantograph.Frontend
|
||||
|
|
@ -3,7 +3,9 @@ Functions for handling metavariables
|
|||
|
||||
All the functions starting with `try` resume their inner monadic state.
|
||||
-/
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Tactic
|
||||
import Pantograph.Compile.Parse
|
||||
import Lean
|
||||
|
||||
|
||||
|
|
@ -46,15 +48,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
|
|||
savedState,
|
||||
parentMVar? := .none,
|
||||
}
|
||||
@[export pantograph_goal_state_create_from_mvars_m]
|
||||
protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
|
||||
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
|
||||
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals } |>.run' {}
|
||||
return {
|
||||
root,
|
||||
savedState,
|
||||
parentMVar? := .none,
|
||||
}
|
||||
@[export pantograph_goal_state_is_conv]
|
||||
protected def GoalState.isConv (state: GoalState): Bool :=
|
||||
state.convMVar?.isSome
|
||||
|
|
@ -152,8 +145,6 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
|
|||
|
||||
@[export pantograph_goal_state_root_expr]
|
||||
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
|
||||
if goalState.root.name == .anonymous then
|
||||
.none
|
||||
let expr ← goalState.mctx.eAssignment.find? goalState.root
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
if expr.hasExprMVar then
|
||||
|
|
@ -394,4 +385,20 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String)
|
|||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
|
||||
|
||||
protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let recursor ← match (← Compile.parseTermM recursor) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
|
||||
protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let eq ← match (← Compile.parseTermM eq) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
|
||||
|
||||
end Pantograph
|
||||
|
|
|
|||
|
|
@ -1,7 +1,8 @@
|
|||
import Pantograph.Condensed
|
||||
import Pantograph.Environment
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Version
|
||||
import Lean
|
||||
|
||||
|
|
@ -41,7 +42,7 @@ namespace Pantograph
|
|||
def runMetaM { α } (metaM: MetaM α): CoreM α :=
|
||||
metaM.run'
|
||||
def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
|
||||
termElabM.run' (ctx := defaultElabContext) |>.run'
|
||||
termElabM.run' (ctx := Condensed.elabContext) |>.run'
|
||||
|
||||
def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
|
||||
|
||||
|
|
@ -158,7 +159,7 @@ def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticRes
|
|||
runTermElabM <| state.tryAssign goal expr
|
||||
@[export pantograph_goal_have_m]
|
||||
protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
|
||||
let type ← match (← parseTermM type) with
|
||||
let type ← match (← Compile.parseTermM type) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
runTermElabM do
|
||||
|
|
@ -166,28 +167,12 @@ protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: S
|
|||
state.tryTacticM goal $ Tactic.evalHave binderName.toName type
|
||||
@[export pantograph_goal_try_define_m]
|
||||
protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
|
||||
let expr ← match (← parseTermM expr) with
|
||||
let expr ← match (← Compile.parseTermM expr) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
runTermElabM do
|
||||
state.restoreElabM
|
||||
state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
|
||||
@[export pantograph_goal_try_motivated_apply_m]
|
||||
protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let recursor ← match (← parseTermM recursor) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
|
||||
@[export pantograph_goal_try_no_confuse_m]
|
||||
protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let eq ← match (← parseTermM eq) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
|
||||
@[export pantograph_goal_let_m]
|
||||
def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryLet goal binderName type
|
||||
|
|
|
|||
|
|
@ -183,12 +183,6 @@ structure EnvAdd where
|
|||
structure EnvAddResult where
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure EnvSaveLoad where
|
||||
path: System.FilePath
|
||||
deriving Lean.FromJson
|
||||
structure EnvSaveLoadResult where
|
||||
deriving Lean.ToJson
|
||||
|
||||
/-- Set options; See `Options` struct above for meanings -/
|
||||
structure OptionsSet where
|
||||
printJsonPretty?: Option Bool
|
||||
|
|
@ -225,7 +219,6 @@ structure GoalTactic where
|
|||
tactic?: Option String := .none
|
||||
expr?: Option String := .none
|
||||
have?: Option String := .none
|
||||
let?: Option String := .none
|
||||
calc?: Option String := .none
|
||||
-- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
|
||||
conv?: Option Bool := .none
|
||||
|
|
@ -291,35 +284,21 @@ structure GoalDiag where
|
|||
|
||||
|
||||
/-- Executes the Lean compiler on a single file -/
|
||||
structure FrontendProcess where
|
||||
-- One of these two must be supplied: Either supply the file name or the content.
|
||||
fileName?: Option String := .none
|
||||
file?: Option String := .none
|
||||
structure CompileUnit where
|
||||
module: String
|
||||
-- If set to true, query the string boundaries of compilation units
|
||||
compilationUnits: Bool := false
|
||||
-- If set to true, collect tactic invocations
|
||||
invocations: Bool := false
|
||||
-- If set to true, collect `sorry`s
|
||||
sorrys: Bool := false
|
||||
deriving Lean.FromJson
|
||||
structure InvokedTactic where
|
||||
goalBefore: String
|
||||
goalAfter: String
|
||||
tactic: String
|
||||
|
||||
-- List of used constants
|
||||
usedConstants: Array String
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure CompilationUnit where
|
||||
-- String boundaries of compilation units
|
||||
boundary: (Nat × Nat)
|
||||
-- Tactic invocations
|
||||
invocations?: Option (List InvokedTactic) := .none
|
||||
goalStateId?: Option Nat := .none
|
||||
goals: Array Goal := #[]
|
||||
messages: Array String := #[]
|
||||
deriving Lean.ToJson
|
||||
structure FrontendProcessResult where
|
||||
units: List CompilationUnit
|
||||
structure CompileUnitResult where
|
||||
units?: Option $ List (Nat × Nat)
|
||||
invocations?: Option $ List InvokedTactic
|
||||
deriving Lean.ToJson
|
||||
|
||||
abbrev CR α := Except InteractionError α
|
||||
|
|
|
|||
|
|
@ -1,73 +1,355 @@
|
|||
import Lean.Environment
|
||||
import Lean.Replay
|
||||
import Init.System.IOError
|
||||
import Std.Data.HashMap
|
||||
|
||||
/-!
|
||||
Input/Output functions
|
||||
|
||||
# Pickling and unpickling objects
|
||||
|
||||
By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk.
|
||||
/-
|
||||
All serialisation functions;
|
||||
This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
|
||||
using `Scope`s.
|
||||
-/
|
||||
import Lean
|
||||
import Pantograph.Condensed
|
||||
import Pantograph.Expr
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Protocol
|
||||
|
||||
open Lean
|
||||
|
||||
-- Symbol processing functions --
|
||||
|
||||
namespace Pantograph
|
||||
|
||||
/--
|
||||
Save an object to disk.
|
||||
If you need to write multiple objects from within a single declaration,
|
||||
you will need to provide a unique `key` for each.
|
||||
-/
|
||||
def pickle {α : Type} (path : System.FilePath) (x : α) (key : Name := by exact decl_name%) : IO Unit :=
|
||||
saveModuleData path key (unsafe unsafeCast x)
|
||||
|
||||
--- Input Functions ---
|
||||
|
||||
/-- Read syntax object from string -/
|
||||
def parseTerm (env: Environment) (s: String): Except String Syntax :=
|
||||
Parser.runParserCategory
|
||||
(env := env)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
/-- Parse a syntax object. May generate additional metavariables! -/
|
||||
def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabType syn
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
|
||||
try
|
||||
let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
|
||||
return .ok expr
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
|
||||
|
||||
--- Output Functions ---
|
||||
|
||||
def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
|
||||
Meta.forallTelescope expr fun arr body => do
|
||||
let binders ← arr.mapM fun fvar => do
|
||||
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
|
||||
return { binders, target := toString (← Meta.ppExpr body) }
|
||||
|
||||
def serializeName (name: Name) (sanitize: Bool := true): String :=
|
||||
let internal := name.isInaccessibleUserName || name.hasMacroScopes
|
||||
if sanitize && internal then "_"
|
||||
else toString name |> addQuotes
|
||||
where
|
||||
addQuotes (n: String) :=
|
||||
let quote := "\""
|
||||
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
|
||||
|
||||
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
|
||||
partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
|
||||
let k := level.getOffset
|
||||
let u := level.getLevelOffset
|
||||
let u_str := match u with
|
||||
| .zero => "0"
|
||||
| .succ _ => panic! "getLevelOffset should not return .succ"
|
||||
| .max v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:max {v} {w})"
|
||||
| .imax v w =>
|
||||
let v := serializeSortLevel v sanitize
|
||||
let w := serializeSortLevel w sanitize
|
||||
s!"(:imax {v} {w})"
|
||||
| .param name =>
|
||||
let name := serializeName name sanitize
|
||||
s!"{name}"
|
||||
| .mvar id =>
|
||||
let name := serializeName id.name sanitize
|
||||
s!"(:mv {name})"
|
||||
match k, u with
|
||||
| 0, _ => u_str
|
||||
| _, .zero => s!"{k}"
|
||||
| _, _ => s!"(+ {u_str} {k})"
|
||||
|
||||
|
||||
/--
|
||||
Load an object from disk.
|
||||
Note: The returned `CompactedRegion` can be used to free the memory behind the value
|
||||
of type `α`, using `CompactedRegion.free` (which is only safe once all references to the `α` are
|
||||
released). Ignoring the `CompactedRegion` results in the data being leaked.
|
||||
Use `withUnpickle` to call `CompactedRegion.free` automatically.
|
||||
Completely serializes an expression tree. Json not used due to compactness
|
||||
|
||||
This function is unsafe because the data being loaded may not actually have type `α`, and this
|
||||
may cause crashes or other bad behavior.
|
||||
A `_` symbol in the AST indicates automatic deductions not present in the original expression.
|
||||
-/
|
||||
unsafe def unpickle (α : Type) (path : System.FilePath) : IO (α × CompactedRegion) := do
|
||||
let (x, region) ← readModuleData path
|
||||
pure (unsafeCast x, region)
|
||||
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
|
||||
self expr
|
||||
where
|
||||
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
|
||||
let .some invocation ← toDelayedMVarInvocation e | return .none
|
||||
let callee ← self $ .mvar invocation.mvarIdPending
|
||||
let sites ← invocation.args.mapM (λ (fvarId, arg) => do
|
||||
let arg := match arg with
|
||||
| .some arg => arg
|
||||
| .none => .fvar fvarId
|
||||
self arg
|
||||
)
|
||||
let tailArgs ← invocation.tail.mapM self
|
||||
|
||||
/-- Load an object from disk and run some continuation on it, freeing memory afterwards. -/
|
||||
unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type}
|
||||
(path : System.FilePath) (f : α → m β) : m β := do
|
||||
let (x, region) ← unpickle α path
|
||||
let r ← f x
|
||||
region.free
|
||||
pure r
|
||||
let sites := " ".intercalate sites.toList
|
||||
let result := if tailArgs.isEmpty then
|
||||
s!"(:subst {callee} {sites})"
|
||||
else
|
||||
let tailArgs := " ".intercalate tailArgs.toList
|
||||
s!"((:subst {callee} {sites}) {tailArgs})"
|
||||
return .some result
|
||||
|
||||
/--
|
||||
Pickle an `Environment` to disk.
|
||||
self (e: Expr): MetaM String := do
|
||||
if let .some result ← delayedMVarToSexp e then
|
||||
return result
|
||||
match e with
|
||||
| .bvar deBruijnIndex =>
|
||||
-- This is very common so the index alone is shown. Literals are handled below.
|
||||
-- The raw de Bruijn index should never appear in an unbound setting. In
|
||||
-- Lean these are handled using a `#` prefix.
|
||||
pure s!"{deBruijnIndex}"
|
||||
| .fvar fvarId =>
|
||||
let name := ofName fvarId.name
|
||||
pure s!"(:fv {name})"
|
||||
| .mvar mvarId => do
|
||||
let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
|
||||
let name := ofName mvarId.name
|
||||
pure s!"(:{pref} {name})"
|
||||
| .sort level =>
|
||||
let level := serializeSortLevel level sanitize
|
||||
pure s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
-- The universe level of the const expression is elided since it should be
|
||||
-- inferrable from surrounding expression
|
||||
pure s!"(:c {declName})"
|
||||
| .app _ _ => do
|
||||
let fn' ← self e.getAppFn
|
||||
let args := (← e.getAppArgs.mapM self) |>.toList
|
||||
let args := " ".intercalate args
|
||||
pure s!"({fn'} {args})"
|
||||
| .lam binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .forallE binderName binderType body binderInfo => do
|
||||
let binderName' := ofName binderName
|
||||
let binderType' ← self binderType
|
||||
let body' ← self body
|
||||
let binderInfo' := binderInfoSexp binderInfo
|
||||
pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
|
||||
| .letE name type value body _ => do
|
||||
-- Dependent boolean flag diacarded
|
||||
let name' := serializeName name
|
||||
let type' ← self type
|
||||
let value' ← self value
|
||||
let body' ← self body
|
||||
pure s!"(:let {name'} {type'} {value'} {body'})"
|
||||
| .lit v =>
|
||||
-- To not burden the downstream parser who needs to handle this, the literal
|
||||
-- is wrapped in a :lit sexp.
|
||||
let v' := match v with
|
||||
| .natVal val => toString val
|
||||
| .strVal val => s!"\"{val}\""
|
||||
pure s!"(:lit {v'})"
|
||||
| .mdata _ inner =>
|
||||
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
|
||||
-- It may become necessary to incorporate the metadata.
|
||||
self inner
|
||||
| .proj _ _ _ => do
|
||||
let env ← getEnv
|
||||
let projApp := exprProjToApp env e
|
||||
let autos := String.intercalate " " (List.replicate projApp.numParams "_")
|
||||
let inner ← self projApp.inner
|
||||
pure s!"((:c {projApp.projector}) {autos} {inner})"
|
||||
-- Elides all unhygenic names
|
||||
binderInfoSexp : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
| .implicit => " :implicit"
|
||||
| .strictImplicit => " :strictImplicit"
|
||||
| .instImplicit => " :instImplicit"
|
||||
ofName (name: Name) := serializeName name sanitize
|
||||
|
||||
We only store:
|
||||
* the list of imports
|
||||
* the new constants from `Environment.constants`
|
||||
and when unpickling, we build a fresh `Environment` from the imports,
|
||||
and then add the new constants.
|
||||
-/
|
||||
@[export pantograph_env_pickle_m]
|
||||
def env_pickle (env : Environment) (path : System.FilePath) : IO Unit :=
|
||||
Pantograph.pickle path (env.header.imports, env.constants.map₂)
|
||||
def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
|
||||
let pp?: Option String ← match options.printExprPretty with
|
||||
| true => pure $ .some $ toString $ ← Meta.ppExpr e
|
||||
| false => pure $ .none
|
||||
let sexp?: Option String ← match options.printExprAST with
|
||||
| true => pure $ .some $ ← serializeExpressionSexp e
|
||||
| false => pure $ .none
|
||||
let dependentMVars? ← match options.printDependentMVars with
|
||||
| true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
|
||||
| false => pure $ .none
|
||||
return {
|
||||
pp?,
|
||||
sexp?
|
||||
dependentMVars?,
|
||||
}
|
||||
|
||||
/--
|
||||
Unpickle an `Environment` from disk.
|
||||
|
||||
We construct a fresh `Environment` with the relevant imports,
|
||||
and then replace the new constants.
|
||||
-/
|
||||
@[export pantograph_env_unpickle_m]
|
||||
def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
|
||||
let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
|
||||
let env ← importModules imports {} 0
|
||||
return (← env.replay (Std.HashMap.ofList map₂.toList), region)
|
||||
/-- Adapted from ppGoal -/
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
|
||||
: MetaM Protocol.Goal := do
|
||||
-- Options for printing; See Meta.ppGoal for details
|
||||
let showLetValues := true
|
||||
let ppAuxDecls := options.printAuxDecls
|
||||
let ppImplDetailHyps := options.printImplementationDetailHyps
|
||||
let lctx := mvarDecl.lctx
|
||||
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
|
||||
Meta.withLCtx lctx mvarDecl.localInstances do
|
||||
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName _ _ _ =>
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
| .cdecl _ fvarId userName type _ _ =>
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
}
|
||||
| .ldecl _ fvarId userName type val _ _ => do
|
||||
let userName := userName.simpMacroScopes
|
||||
let type ← instantiate type
|
||||
let value? ← if showLetValues then
|
||||
let val ← instantiate val
|
||||
pure $ .some (← serializeExpression options val)
|
||||
else
|
||||
pure $ .none
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
value? := value?
|
||||
}
|
||||
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
|
||||
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
|
||||
!ppImplDetailHyps && localDecl.isImplementationDetail
|
||||
if skip then
|
||||
return acc
|
||||
else
|
||||
let nameOnly := options.noRepeat && (parentDecl?.map
|
||||
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
|
||||
let var ← match nameOnly with
|
||||
| true => ppVarNameOnly localDecl
|
||||
| false => ppVar localDecl
|
||||
return var::acc
|
||||
return {
|
||||
name := ofName goal.name,
|
||||
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
|
||||
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
|
||||
target := (← serializeExpression options (← instantiate mvarDecl.type)),
|
||||
vars := vars.reverse.toArray
|
||||
}
|
||||
where
|
||||
instantiate := instantiateAll
|
||||
ofName (n: Name) := serializeName n (sanitize := false)
|
||||
|
||||
protected def GoalState.serializeGoals
|
||||
(state: GoalState)
|
||||
(parent: Option GoalState := .none)
|
||||
(options: @&Protocol.Options := {}):
|
||||
MetaM (Array Protocol.Goal):= do
|
||||
state.restoreMetaM
|
||||
let goals := state.goals.toArray
|
||||
let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
|
||||
goals.mapM fun goal => do
|
||||
match state.mctx.findDecl? goal with
|
||||
| .some mvarDecl =>
|
||||
let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
|
||||
pure serializedGoal
|
||||
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
|
||||
|
||||
/-- Print the metavariables in a readable format -/
|
||||
@[export pantograph_goal_state_diag_m]
|
||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
|
||||
let metaM: MetaM String := do
|
||||
goalState.restoreMetaM
|
||||
let savedState := goalState.savedState
|
||||
let goals := savedState.tactic.goals
|
||||
let mctx ← getMCtx
|
||||
let root := goalState.root
|
||||
-- Print the root
|
||||
let result: String ← match mctx.decls.find? root with
|
||||
| .some decl => printMVar ">" root decl
|
||||
| .none => pure s!">{root.name}: ??"
|
||||
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
|
||||
match mctx.decls.find? mvarId with
|
||||
| .some decl => printMVar "⊢" mvarId decl
|
||||
| .none => pure s!"⊢{mvarId.name}: ??"
|
||||
)
|
||||
let goals := goals.toSSet
|
||||
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
|
||||
!(goals.contains mvarId || mvarId == root) && options.printAll)
|
||||
|>.mapM (fun (mvarId, decl) => do
|
||||
let pref := if parentHasMVar mvarId then " " else "~"
|
||||
printMVar pref mvarId decl
|
||||
)
|
||||
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
||||
metaM.run' {}
|
||||
where
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
||||
let resultFVars: List String ←
|
||||
if options.printContext then
|
||||
decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
|
||||
do pure $ (← printFVar fvarId decl) ++ "\n")
|
||||
else
|
||||
pure []
|
||||
let type ← if options.instantiate
|
||||
then instantiateAll decl.type
|
||||
else pure $ decl.type
|
||||
let type_sexp ← if options.printSexp then
|
||||
let sexp ← serializeExpressionSexp type (sanitize := false)
|
||||
pure <| " " ++ sexp
|
||||
else
|
||||
pure ""
|
||||
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
|
||||
let resultValue: String ←
|
||||
if options.printValue then
|
||||
if let .some value ← getExprMVarAssignment? mvarId then
|
||||
let value ← if options.instantiate
|
||||
then instantiateAll value
|
||||
else pure $ value
|
||||
pure s!"\n := {← Meta.ppExpr value}"
|
||||
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
|
||||
pure s!"\n ::= {mvarIdPending.name}"
|
||||
else
|
||||
pure ""
|
||||
else
|
||||
pure ""
|
||||
pure $ (String.join resultFVars) ++ resultMain ++ resultValue
|
||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
|
||||
pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||
userNameToString : Name → String
|
||||
| .anonymous => ""
|
||||
| other => s!"[{other}]"
|
||||
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
|
||||
|
||||
end Pantograph
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
namespace Pantograph
|
||||
|
||||
@[export pantograph_version]
|
||||
def version := "0.2.19"
|
||||
def version := "0.2.18"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
|||
72
README.md
72
README.md
|
|
@ -9,17 +9,30 @@ examine the symbol list of a Lean project for machine learning.
|
|||
|
||||
## Installation
|
||||
|
||||
For Nix users, run
|
||||
``` sh
|
||||
nix build .#{sharedLib,executable}
|
||||
```
|
||||
to build either the shared library or executable.
|
||||
For Nix based workflow, see below.
|
||||
|
||||
Install `elan` and `lake`, and run
|
||||
``` sh
|
||||
lake build
|
||||
```
|
||||
This builds the executable in `.lake/build/bin/pantograph-repl`.
|
||||
This builds the executable in `.lake/build/bin/pantograph`.
|
||||
|
||||
To use Pantograph in a project environment, setup the `LEAN_PATH` environment
|
||||
variable so it contains the library path of lean libraries. The libraries must
|
||||
be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
|
||||
the environment might be setup like this:
|
||||
|
||||
``` sh
|
||||
LIB="../lib"
|
||||
LIB_MATHLIB="$LIB/mathlib4/lake-packages"
|
||||
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
|
||||
|
||||
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
|
||||
```
|
||||
The `$LEAN_PATH` executable of any project can be extracted by
|
||||
``` sh
|
||||
lake env printenv LEAN_PATH
|
||||
```
|
||||
|
||||
## Executable Usage
|
||||
|
||||
|
|
@ -101,10 +114,6 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
|
|||
- `{ "goals": <names> }`: Resume the given goals
|
||||
* `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
|
||||
* `goal.print {"stateId": <id>}"`: Print a goal state
|
||||
* `frontend.process { ["fileName": <fileName>",] ["file": <str>], invocations:
|
||||
<bool>, sorrys: <bool> }`: Executes the Lean frontend on a file, collecting
|
||||
either the tactic invocations (`"invocations": true`) or the sorrys into goal
|
||||
states (`"sorrys": true`)
|
||||
|
||||
### Errors
|
||||
|
||||
|
|
@ -121,25 +130,6 @@ Common error forms:
|
|||
input of another is broken. For example, attempting to query a symbol not
|
||||
existing in the library or indexing into a non-existent proof state.
|
||||
|
||||
### Project Environment
|
||||
|
||||
To use Pantograph in a project environment, setup the `LEAN_PATH` environment
|
||||
variable so it contains the library path of lean libraries. The libraries must
|
||||
be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
|
||||
the environment might be setup like this:
|
||||
|
||||
``` sh
|
||||
LIB="../lib"
|
||||
LIB_MATHLIB="$LIB/mathlib4/lake-packages"
|
||||
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
|
||||
|
||||
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
|
||||
```
|
||||
The `$LEAN_PATH` executable of any project can be extracted by
|
||||
``` sh
|
||||
lake env printenv LEAN_PATH
|
||||
```
|
||||
|
||||
### Troubleshooting
|
||||
|
||||
If lean encounters stack overflow problems when printing catalog, execute this before running lean:
|
||||
|
|
@ -153,11 +143,8 @@ ulimit -s unlimited
|
|||
with `Pantograph` which mirrors the REPL commands above. It is recommended to
|
||||
call Pantograph via this FFI since it provides a tremendous speed up.
|
||||
|
||||
The executable can be used as-is, but linking against the shared library
|
||||
requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence
|
||||
between executable (REPL) commands and library functions.
|
||||
|
||||
Inject any project path via the `pantograph_init_search` function.
|
||||
Note that there isn't a 1-1 correspondence between executable (REPL) commands
|
||||
and library functions.
|
||||
|
||||
## Developing
|
||||
|
||||
|
|
@ -165,11 +152,7 @@ A Lean development shell is provided in the Nix flake.
|
|||
|
||||
### Testing
|
||||
|
||||
The tests are based on `LSpec`. To run tests, use either
|
||||
``` sh
|
||||
nix flake check
|
||||
```
|
||||
or
|
||||
The tests are based on `LSpec`. To run tests,
|
||||
``` sh
|
||||
lake test
|
||||
```
|
||||
|
|
@ -178,3 +161,14 @@ You can run an individual test by specifying a prefix
|
|||
``` sh
|
||||
lake test -- "Tactic/No Confuse"
|
||||
```
|
||||
|
||||
## Nix based workflow
|
||||
|
||||
The included Nix flake provides build targets for `sharedLib` and `executable`.
|
||||
The executable can be used as-is, but linking against the shared library
|
||||
requires the presence of `lean-all`.
|
||||
|
||||
To run tests:
|
||||
``` sh
|
||||
nix flake check
|
||||
```
|
||||
|
|
|
|||
182
Repl.lean
182
Repl.lean
|
|
@ -1,7 +1,7 @@
|
|||
import Std.Data.HashMap
|
||||
import Lean.Data.HashMap
|
||||
import Pantograph
|
||||
|
||||
namespace Pantograph.Repl
|
||||
namespace Pantograph
|
||||
|
||||
structure Context where
|
||||
imports: List String
|
||||
|
|
@ -10,7 +10,7 @@ structure Context where
|
|||
structure State where
|
||||
options: Protocol.Options := {}
|
||||
nextId: Nat := 0
|
||||
goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
|
||||
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
|
||||
|
||||
/-- Main state monad for executing commands -/
|
||||
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
|
||||
|
|
@ -22,9 +22,8 @@ abbrev CR α := Except Protocol.InteractionError α
|
|||
def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
|
||||
metaM.run'
|
||||
def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
|
||||
termElabM.run' (ctx := defaultElabContext) |>.run'
|
||||
termElabM.run' (ctx := Condensed.elabContext) |>.run'
|
||||
|
||||
/-- Main loop command of the REPL -/
|
||||
def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
|
||||
match Lean.fromJson? command.payload with
|
||||
|
|
@ -33,48 +32,33 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
| .ok result => return Lean.toJson result
|
||||
| .error ierror => return Lean.toJson ierror
|
||||
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
|
||||
try
|
||||
match command.cmd with
|
||||
| "reset" => run reset
|
||||
| "stat" => run stat
|
||||
| "expr.echo" => run expr_echo
|
||||
| "env.catalog" => run env_catalog
|
||||
| "env.inspect" => run env_inspect
|
||||
| "env.add" => run env_add
|
||||
| "env.save" => run env_save
|
||||
| "env.load" => run env_load
|
||||
| "options.set" => run options_set
|
||||
| "options.print" => run options_print
|
||||
| "goal.start" => run goal_start
|
||||
| "goal.tactic" => run goal_tactic
|
||||
| "goal.continue" => run goal_continue
|
||||
| "goal.delete" => run goal_delete
|
||||
| "goal.print" => run goal_print
|
||||
| "frontend.process" => run frontend_process
|
||||
| cmd =>
|
||||
let error: Protocol.InteractionError :=
|
||||
errorCommand s!"Unknown command {cmd}"
|
||||
return Lean.toJson error
|
||||
catch ex => do
|
||||
let error ← ex.toMessageData.toString
|
||||
return Lean.toJson $ errorIO error
|
||||
match command.cmd with
|
||||
| "reset" => run reset
|
||||
| "stat" => run stat
|
||||
| "expr.echo" => run expr_echo
|
||||
| "env.catalog" => run env_catalog
|
||||
| "env.inspect" => run env_inspect
|
||||
| "env.add" => run env_add
|
||||
| "options.set" => run options_set
|
||||
| "options.print" => run options_print
|
||||
| "goal.start" => run goal_start
|
||||
| "goal.tactic" => run goal_tactic
|
||||
| "goal.continue" => run goal_continue
|
||||
| "goal.delete" => run goal_delete
|
||||
| "goal.print" => run goal_print
|
||||
| "compile.unit" => run compile_unit
|
||||
| cmd =>
|
||||
let error: Protocol.InteractionError :=
|
||||
errorCommand s!"Unknown command {cmd}"
|
||||
return Lean.toJson error
|
||||
where
|
||||
errorCommand := errorI "command"
|
||||
errorIndex := errorI "index"
|
||||
errorIO := errorI "io"
|
||||
newGoalState (goalState: GoalState) : MainM Nat := do
|
||||
let state ← get
|
||||
let stateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert stateId goalState,
|
||||
nextId := state.nextId + 1
|
||||
}
|
||||
return stateId
|
||||
-- Command Functions
|
||||
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
|
||||
let state ← get
|
||||
let nGoals := state.goalStates.size
|
||||
set { state with nextId := 0, goalStates := .empty }
|
||||
set { state with nextId := 0, goalStates := Lean.HashMap.empty }
|
||||
return .ok { nGoals }
|
||||
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
|
||||
let state ← get
|
||||
|
|
@ -88,14 +72,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
Environment.inspect args state.options
|
||||
env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
|
||||
Environment.addDecl args
|
||||
env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
env_pickle env args.path
|
||||
return .ok {}
|
||||
env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
|
||||
let (env, _) ← env_unpickle args.path
|
||||
Lean.setEnv env
|
||||
return .ok {}
|
||||
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
|
||||
let state ← get
|
||||
exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
|
||||
|
|
@ -119,6 +95,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
|
||||
return .ok (← get).options
|
||||
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
|
||||
let state ← get
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
|
||||
| .some expr, .none => goalStartExpr expr (args.levels.getD #[])
|
||||
|
|
@ -131,33 +108,34 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
match expr? with
|
||||
| .error error => return .error error
|
||||
| .ok goalState =>
|
||||
let stateId ← newGoalState goalState
|
||||
let stateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert stateId goalState,
|
||||
nextId := state.nextId + 1
|
||||
}
|
||||
return .ok { stateId, root := goalState.root.name.toString }
|
||||
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
|
||||
let state ← get
|
||||
let .some goalState := state.goalStates[args.stateId]? |
|
||||
let .some goalState := state.goalStates.find? args.stateId |
|
||||
return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
let .some goal := goalState.goals.get? args.goalId |
|
||||
return .error $ errorIndex s!"Invalid goal index {args.goalId}"
|
||||
let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
|
||||
match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv? with
|
||||
| .some tactic, .none, .none, .none, .none, .none => do
|
||||
match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with
|
||||
| .some tactic, .none, .none, .none, .none => do
|
||||
pure <| Except.ok <| ← goalState.tryTactic goal tactic
|
||||
| .none, .some expr, .none, .none, .none, .none => do
|
||||
| .none, .some expr, .none, .none, .none => do
|
||||
pure <| Except.ok <| ← goalState.tryAssign goal expr
|
||||
| .none, .none, .some type, .none, .none, .none => do
|
||||
| .none, .none, .some type, .none, .none => do
|
||||
let binderName := args.binderName?.getD ""
|
||||
pure <| Except.ok <| ← goalState.tryHave goal binderName type
|
||||
| .none, .none, .none, .some type, .none, .none => do
|
||||
let binderName := args.binderName?.getD ""
|
||||
pure <| Except.ok <| ← goalState.tryLet goal binderName type
|
||||
| .none, .none, .none, .none, .some pred, .none => do
|
||||
| .none, .none, .none, .some pred, .none => do
|
||||
pure <| Except.ok <| ← goalState.tryCalc goal pred
|
||||
| .none, .none, .none, .none, .none, .some true => do
|
||||
| .none, .none, .none, .none, .some true => do
|
||||
pure <| Except.ok <| ← goalState.conv goal
|
||||
| .none, .none, .none, .none, .none, .some false => do
|
||||
| .none, .none, .none, .none, .some false => do
|
||||
pure <| Except.ok <| ← goalState.convExit
|
||||
| _, _, _, _, _, _ =>
|
||||
| _, _, _, _, _ =>
|
||||
let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
|
||||
pure $ Except.error $ error
|
||||
match nextGoalState? with
|
||||
|
|
@ -165,18 +143,19 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
| .ok (.success nextGoalState) => do
|
||||
let nextGoalState ← match state.options.automaticMode, args.conv? with
|
||||
| true, .none => do
|
||||
let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
|
||||
throwError "Resuming known goals"
|
||||
let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) | throwError "Resuming known goals"
|
||||
pure result
|
||||
| true, .some true => pure nextGoalState
|
||||
| true, .some false => do
|
||||
let .some (_, _, dormantGoals) := goalState.convMVar? |
|
||||
throwError "If conv exit succeeded this should not fail"
|
||||
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
|
||||
throwError "Resuming known goals"
|
||||
let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail"
|
||||
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals"
|
||||
pure result
|
||||
| false, _ => pure nextGoalState
|
||||
let nextStateId ← newGoalState nextGoalState
|
||||
let nextStateId := state.nextId
|
||||
set { state with
|
||||
goalStates := state.goalStates.insert state.nextId nextGoalState,
|
||||
nextId := state.nextId + 1,
|
||||
}
|
||||
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
|
||||
return .ok {
|
||||
nextStateId? := .some nextStateId,
|
||||
|
|
@ -190,11 +169,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
return .ok { tacticErrors? := .some messages }
|
||||
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
|
||||
let state ← get
|
||||
let .some target := state.goalStates[args.target]? |
|
||||
return .error $ errorIndex s!"Invalid state index {args.target}"
|
||||
let .some target := state.goalStates.find? args.target | return .error $ errorIndex s!"Invalid state index {args.target}"
|
||||
let nextState? ← match args.branch?, args.goals? with
|
||||
| .some branchId, .none => do
|
||||
match state.goalStates[branchId]? with
|
||||
match state.goalStates.find? branchId with
|
||||
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
|
||||
| .some branch => pure $ target.continue branch
|
||||
| .none, .some goals =>
|
||||
|
|
@ -220,57 +198,23 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
return .ok {}
|
||||
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
|
||||
let state ← get
|
||||
let .some goalState := state.goalStates[args.stateId]? |
|
||||
return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}"
|
||||
let result ← runMetaInMainM <| goalPrint goalState state.options
|
||||
return .ok result
|
||||
frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
|
||||
let options := (← get).options
|
||||
compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
|
||||
let module := args.module.toName
|
||||
try
|
||||
let (fileName, file) ← match args.fileName?, args.file? with
|
||||
| .some fileName, .none => do
|
||||
let file ← IO.FS.readFile fileName
|
||||
pure (fileName, file)
|
||||
| .none, .some file =>
|
||||
pure ("<anonymous>", file)
|
||||
| _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
|
||||
let env?: Option Lean.Environment ← if args.fileName?.isSome then
|
||||
let steps ← Compile.processSource module
|
||||
let units? := if args.compilationUnits then
|
||||
.some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
|
||||
else
|
||||
.none
|
||||
let invocations? ← if args.invocations then
|
||||
pure $ .some (← Compile.collectTacticsFromCompilation steps)
|
||||
else
|
||||
pure .none
|
||||
else do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
pure <| .some env
|
||||
let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
|
||||
let frontendM := Frontend.mapCompilationSteps λ step => do
|
||||
let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
|
||||
let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
|
||||
let invocations ← Frontend.collectTacticsFromCompilationStep step
|
||||
pure $ .some invocations
|
||||
else
|
||||
pure .none
|
||||
let sorrys := if args.sorrys then
|
||||
Frontend.collectSorrys step
|
||||
else
|
||||
[]
|
||||
let messages ← step.messageStrings
|
||||
return (step.before, boundary, invocations?, sorrys, messages)
|
||||
let li ← frontendM.run context |>.run' state
|
||||
let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do
|
||||
let (goalStateId?, goals) ← if sorrys.isEmpty then do
|
||||
pure (.none, #[])
|
||||
else do
|
||||
let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
|
||||
let stateId ← newGoalState goalState
|
||||
let goals ← goalSerialize goalState options
|
||||
pure (.some stateId, goals)
|
||||
return {
|
||||
boundary,
|
||||
invocations?,
|
||||
goalStateId?,
|
||||
goals,
|
||||
messages,
|
||||
}
|
||||
return .ok { units }
|
||||
return .ok { units?, invocations? }
|
||||
catch e =>
|
||||
return .error $ errorI "frontend" (← e.toMessageData.toString)
|
||||
return .error $ errorI "compile" (← e.toMessageData.toString)
|
||||
|
||||
end Pantograph.Repl
|
||||
end Pantograph
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
import Pantograph.Goal
|
||||
import Pantograph.Library
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Condensed
|
||||
import Lean
|
||||
import LSpec
|
||||
|
||||
|
|
@ -89,9 +90,9 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
|
|||
def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runCoreMSeq env metaM.run'
|
||||
def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
|
||||
termElabM.run' (ctx := defaultElabContext)
|
||||
termElabM.run' (ctx := Condensed.elabContext)
|
||||
def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
|
||||
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
|
||||
|
||||
def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
import LSpec
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Environment
|
||||
import Test.Common
|
||||
import Lean
|
||||
|
|
@ -33,7 +33,7 @@ def test_catalog: IO LSpec.TestSeq := do
|
|||
def test_symbol_visibility: IO LSpec.TestSeq := do
|
||||
let entries: List (Name × Bool) := [
|
||||
("Nat.add_comm".toName, false),
|
||||
("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
|
||||
("Lean.Name".toName, true),
|
||||
("Init.Data.Nat.Basic._auxLemma.4".toName, true),
|
||||
]
|
||||
let suite := entries.foldl (λ suites (symbol, target) =>
|
||||
|
|
|
|||
|
|
@ -1,191 +0,0 @@
|
|||
import LSpec
|
||||
import Pantograph
|
||||
import Repl
|
||||
import Test.Common
|
||||
|
||||
open Lean Pantograph
|
||||
namespace Pantograph.Test.Frontend
|
||||
|
||||
def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
|
||||
let filename := "<anonymous>"
|
||||
let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
|
||||
let m := Frontend.mapCompilationSteps λ step => do
|
||||
return (step.before, Frontend.collectSorrys step)
|
||||
let li ← m.run context |>.run' state
|
||||
let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
|
||||
if sorrys.isEmpty then
|
||||
return .none
|
||||
let goalState ← Frontend.sorrysToGoalState sorrys
|
||||
return .some goalState
|
||||
return goalStates
|
||||
|
||||
def test_multiple_sorrys_in_proof : TestT MetaM Unit := do
|
||||
let sketch := "
|
||||
theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by
|
||||
have h_nat_add_succ: ∀ n m : Nat, n = m := sorry
|
||||
sorry
|
||||
"
|
||||
let goalStates ← (collectSorrysFromSource sketch).run' {}
|
||||
let [goalState] := goalStates | panic! "Incorrect number of states"
|
||||
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
|
||||
{
|
||||
target := { pp? := "∀ (n m : Nat), n = m" },
|
||||
vars := #[
|
||||
]
|
||||
},
|
||||
{
|
||||
target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" },
|
||||
vars := #[{
|
||||
userName := "h_nat_add_succ",
|
||||
type? := .some { pp? := "∀ (n m : Nat), n = m" },
|
||||
}],
|
||||
}
|
||||
])
|
||||
|
||||
def test_sorry_in_middle: TestT MetaM Unit := do
|
||||
let sketch := "
|
||||
example : ∀ (n m: Nat), n + m = m + n := by
|
||||
intros n m
|
||||
sorry
|
||||
"
|
||||
let goalStates ← (collectSorrysFromSource sketch).run' {}
|
||||
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
|
||||
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
|
||||
{
|
||||
target := { pp? := "n + m = m + n" },
|
||||
vars := #[{
|
||||
userName := "n",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}, {
|
||||
userName := "m",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}
|
||||
],
|
||||
}
|
||||
])
|
||||
|
||||
def test_sorry_in_induction : TestT MetaM Unit := do
|
||||
let sketch := "
|
||||
example : ∀ (n m: Nat), n + m = m + n := by
|
||||
intros n m
|
||||
induction n with
|
||||
| zero =>
|
||||
have h1 : 0 + m = m := sorry
|
||||
sorry
|
||||
| succ n ih =>
|
||||
have h2 : n + m = m := sorry
|
||||
sorry
|
||||
"
|
||||
let goalStates ← (collectSorrysFromSource sketch).run' {}
|
||||
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
|
||||
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
|
||||
{
|
||||
target := { pp? := "0 + m = m" },
|
||||
vars := #[{
|
||||
userName := "m",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}]
|
||||
},
|
||||
{
|
||||
userName? := .some "zero",
|
||||
target := { pp? := "0 + m = m + 0" },
|
||||
vars := #[{
|
||||
userName := "m",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}, {
|
||||
userName := "h1",
|
||||
type? := .some { pp? := "0 + m = m" },
|
||||
}]
|
||||
},
|
||||
{
|
||||
target := { pp? := "n + m = m" },
|
||||
vars := #[{
|
||||
userName := "m",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}, {
|
||||
userName := "n",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}, {
|
||||
userName := "ih",
|
||||
type? := .some { pp? := "n + m = m + n" },
|
||||
}]
|
||||
},
|
||||
{
|
||||
userName? := .some "succ",
|
||||
target := { pp? := "n + 1 + m = m + (n + 1)" },
|
||||
vars := #[{
|
||||
userName := "m",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}, {
|
||||
userName := "n",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}, {
|
||||
userName := "ih",
|
||||
type? := .some { pp? := "n + m = m + n" },
|
||||
}, {
|
||||
userName := "h2",
|
||||
type? := .some { pp? := "n + m = m" },
|
||||
}]
|
||||
}
|
||||
])
|
||||
|
||||
def test_sorry_in_coupled: TestT MetaM Unit := do
|
||||
let sketch := "
|
||||
example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
|
||||
intro y
|
||||
apply Exists.intro
|
||||
case h => sorry
|
||||
case w => sorry
|
||||
"
|
||||
let goalStates ← (collectSorrysFromSource sketch).run' {}
|
||||
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
|
||||
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
|
||||
{
|
||||
target := { pp? := "y + 1 = ?w" },
|
||||
vars := #[{
|
||||
userName := "y",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}
|
||||
],
|
||||
},
|
||||
{
|
||||
userName? := .some "w",
|
||||
target := { pp? := "Nat" },
|
||||
vars := #[{
|
||||
userName := "y",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}
|
||||
],
|
||||
}
|
||||
])
|
||||
|
||||
def test_environment_capture: TestT MetaM Unit := do
|
||||
let sketch := "
|
||||
def mystery (n: Nat) := n + 1
|
||||
|
||||
example (n: Nat) : mystery n + 1 = n + 2 := sorry
|
||||
"
|
||||
let goalStates ← (collectSorrysFromSource sketch).run' {}
|
||||
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
|
||||
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
|
||||
{
|
||||
target := { pp? := "mystery n + 1 = n + 2" },
|
||||
vars := #[{
|
||||
userName := "n",
|
||||
type? := .some { pp? := "Nat" },
|
||||
}],
|
||||
}
|
||||
])
|
||||
|
||||
|
||||
def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
|
||||
let tests := [
|
||||
("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
|
||||
("sorry_in_middle", test_sorry_in_middle),
|
||||
("sorry_in_induction", test_sorry_in_induction),
|
||||
("sorry_in_coupled", test_sorry_in_coupled),
|
||||
("environment_capture", test_environment_capture),
|
||||
]
|
||||
tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
|
||||
|
||||
end Pantograph.Test.Frontend
|
||||
|
|
@ -6,13 +6,13 @@ import Repl
|
|||
import Test.Common
|
||||
|
||||
namespace Pantograph.Test.Integration
|
||||
open Pantograph.Repl
|
||||
open Pantograph
|
||||
|
||||
def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
|
||||
(expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
|
||||
let payload := Lean.Json.mkObj payload
|
||||
let name := name?.getD s!"{cmd} {payload.compress}"
|
||||
let result ← Repl.execute { cmd, payload }
|
||||
let result ← execute { cmd, payload }
|
||||
return LSpec.test name (toString result = toString (Lean.toJson expected))
|
||||
|
||||
abbrev Test := List (MainM LSpec.TestSeq)
|
||||
|
|
@ -161,73 +161,6 @@ def test_env_add_inspect : Test :=
|
|||
Protocol.EnvInspectResult)
|
||||
]
|
||||
|
||||
example : ∀ (p: Prop), p → p := by
|
||||
intro p h
|
||||
exact h
|
||||
|
||||
def test_frontend_process : Test :=
|
||||
[
|
||||
let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n intro p q h\n exact Or.inl h"
|
||||
let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
|
||||
step "frontend.process"
|
||||
[
|
||||
("file", .str file),
|
||||
("invocations", .bool true),
|
||||
("sorrys", .bool false),
|
||||
]
|
||||
({
|
||||
units := [{
|
||||
boundary := (0, file.utf8ByteSize),
|
||||
invocations? := .some [
|
||||
{
|
||||
goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
|
||||
goalAfter := goal1,
|
||||
tactic := "intro p q h",
|
||||
usedConstants := #[],
|
||||
},
|
||||
{
|
||||
goalBefore := goal1 ,
|
||||
goalAfter := "",
|
||||
tactic := "exact Or.inl h",
|
||||
usedConstants := #["Or.inl"],
|
||||
},
|
||||
]
|
||||
}],
|
||||
}: Protocol.FrontendProcessResult),
|
||||
]
|
||||
|
||||
example : 1 + 2 = 3 := rfl
|
||||
example (p: Prop): p → p := by simp
|
||||
|
||||
def test_frontend_process_sorry : Test :=
|
||||
let solved := "example : 1 + 2 = 3 := rfl\n"
|
||||
let withSorry := "example (p: Prop): p → p := sorry"
|
||||
[
|
||||
let file := s!"{solved}{withSorry}"
|
||||
let goal1: Protocol.Goal := {
|
||||
name := "_uniq.6",
|
||||
target := { pp? := .some "p → p" },
|
||||
vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
|
||||
}
|
||||
step "frontend.process"
|
||||
[
|
||||
("file", .str file),
|
||||
("invocations", .bool false),
|
||||
("sorrys", .bool true),
|
||||
]
|
||||
({
|
||||
units := [{
|
||||
boundary := (0, solved.utf8ByteSize),
|
||||
}, {
|
||||
boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
|
||||
goalStateId? := .some 0,
|
||||
goals := #[goal1],
|
||||
messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
|
||||
}],
|
||||
}: Protocol.FrontendProcessResult),
|
||||
]
|
||||
|
||||
|
||||
def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
|
||||
-- Setup the environment for execution
|
||||
let context: Context := {
|
||||
|
|
@ -249,8 +182,6 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
|
|||
("Manual Mode", test_automatic_mode false),
|
||||
("Automatic Mode", test_automatic_mode true),
|
||||
("env.add env.inspect", test_env_add_inspect),
|
||||
("frontend.process invocation", test_frontend_process),
|
||||
("frontend.process sorry", test_frontend_process_sorry),
|
||||
]
|
||||
tests.map (fun (name, test) => (name, runTest env test))
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,10 @@
|
|||
import LSpec
|
||||
import Test.Environment
|
||||
import Test.Frontend
|
||||
import Test.Integration
|
||||
import Test.Library
|
||||
import Test.Metavar
|
||||
import Test.Proofs
|
||||
import Test.Delate
|
||||
import Test.Serial
|
||||
import Test.Tactic
|
||||
|
||||
-- Test running infrastructure
|
||||
|
|
@ -45,12 +44,11 @@ def main (args: List String) := do
|
|||
|
||||
let suites: List (String × List (String × IO LSpec.TestSeq)) := [
|
||||
("Environment", Environment.suite),
|
||||
("Frontend", Frontend.suite env_default),
|
||||
("Integration", Integration.suite env_default),
|
||||
("Library", Library.suite env_default),
|
||||
("Metavar", Metavar.suite env_default),
|
||||
("Proofs", Proofs.suite env_default),
|
||||
("Delate", Delate.suite env_default),
|
||||
("Serial", Serial.suite env_default),
|
||||
("Tactic/Congruence", Tactic.Congruence.suite env_default),
|
||||
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
|
||||
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
import LSpec
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Serial
|
||||
import Test.Common
|
||||
import Lean
|
||||
|
||||
|
|
@ -66,7 +66,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
|
|||
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
|
||||
|
||||
let coreContext: Lean.Core.Context ← createCoreContext #[]
|
||||
let metaM := termElabM.run' (ctx := defaultElabContext)
|
||||
let metaM := termElabM.run' (ctx := Condensed.elabContext)
|
||||
let coreM := metaM.run'
|
||||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ Tests pertaining to goals with no interdependencies
|
|||
-/
|
||||
import LSpec
|
||||
import Pantograph.Goal
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Serial
|
||||
import Test.Common
|
||||
|
||||
namespace Pantograph.Test.Proofs
|
||||
|
|
@ -74,7 +74,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
|
|||
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
|
||||
|
||||
let coreContext: Lean.Core.Context ← createCoreContext #[]
|
||||
let metaM := termElabM.run' (ctx := defaultElabContext)
|
||||
let metaM := termElabM.run' (ctx := Condensed.elabContext)
|
||||
let coreM := metaM.run'
|
||||
match ← (coreM.run' coreContext { env := env }).toBaseIO with
|
||||
| .error exception =>
|
||||
|
|
|
|||
|
|
@ -1,10 +1,10 @@
|
|||
import LSpec
|
||||
import Pantograph.Delate
|
||||
import Pantograph.Serial
|
||||
import Test.Common
|
||||
import Lean
|
||||
|
||||
open Lean
|
||||
namespace Pantograph.Test.Delate
|
||||
namespace Pantograph.Test.Serial
|
||||
|
||||
open Pantograph
|
||||
|
||||
|
|
@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
|
|||
| .ok expr => pure expr
|
||||
| .error e => return elabFailure e
|
||||
return LSpec.check source ((← serializeExpressionSexp expr) = target)
|
||||
let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultElabContext)
|
||||
let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
|
||||
return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
|
||||
LSpec.TestSeq.done
|
||||
|
||||
|
|
@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
|
|||
let testCaseName := target.take 10
|
||||
let test := LSpec.check testCaseName ((← serializeExpressionSexp expr) = target)
|
||||
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
|
||||
runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
|
||||
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
|
||||
|
||||
-- Instance parsing
|
||||
def test_instance (env: Environment): IO LSpec.TestSeq :=
|
||||
|
|
@ -106,4 +106,4 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
|||
("Instance", test_instance env),
|
||||
]
|
||||
|
||||
end Pantograph.Test.Delate
|
||||
end Pantograph.Test.Serial
|
||||
206
flake.lock
206
flake.lock
|
|
@ -5,11 +5,11 @@
|
|||
"nixpkgs-lib": "nixpkgs-lib"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1730504689,
|
||||
"narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=",
|
||||
"lastModified": 1709336216,
|
||||
"narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"rev": "506278e768c2a08bec68eb62932193e341f55c90",
|
||||
"rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
|
|
@ -18,112 +18,208 @@
|
|||
"type": "github"
|
||||
}
|
||||
},
|
||||
"flake-parts_2": {
|
||||
"inputs": {
|
||||
"nixpkgs-lib": "nixpkgs-lib_2"
|
||||
},
|
||||
"flake-utils": {
|
||||
"locked": {
|
||||
"lastModified": 1727826117,
|
||||
"narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
|
||||
"lastModified": 1656928814,
|
||||
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "hercules-ci",
|
||||
"repo": "flake-parts",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lean4-nix": {
|
||||
"lean": {
|
||||
"inputs": {
|
||||
"flake-parts": "flake-parts_2",
|
||||
"nixpkgs": "nixpkgs"
|
||||
"flake-utils": "flake-utils",
|
||||
"lean4-mode": "lean4-mode",
|
||||
"nix": "nix",
|
||||
"nixpkgs": "nixpkgs_2",
|
||||
"nixpkgs-old": "nixpkgs-old"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1731711316,
|
||||
"narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
|
||||
"owner": "lenianiva",
|
||||
"repo": "lean4-nix",
|
||||
"rev": "136fc6057c48de970579e960b62421e9c295b67d",
|
||||
"lastModified": 1719788866,
|
||||
"narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=",
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4",
|
||||
"rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "lenianiva",
|
||||
"repo": "lean4-nix",
|
||||
"owner": "leanprover",
|
||||
"ref": "v4.10.0-rc1",
|
||||
"repo": "lean4",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lean4-mode": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1676498134,
|
||||
"narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4-mode",
|
||||
"rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "leanprover",
|
||||
"repo": "lean4-mode",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lowdown-src": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1633514407,
|
||||
"narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
|
||||
"owner": "kristapsdz",
|
||||
"repo": "lowdown",
|
||||
"rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "kristapsdz",
|
||||
"repo": "lowdown",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"lspec": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1728279187,
|
||||
"narHash": "sha256-ZMqbvCqR/gHXRuIkuo7b0Yp9N1vOQR7xnrcy/SeIBoQ=",
|
||||
"owner": "argumentcomputer",
|
||||
"lastModified": 1722857503,
|
||||
"narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=",
|
||||
"owner": "lurk-lab",
|
||||
"repo": "LSpec",
|
||||
"rev": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
|
||||
"rev": "8a51034d049c6a229d88dd62f490778a377eec06",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "argumentcomputer",
|
||||
"ref": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
|
||||
"owner": "lurk-lab",
|
||||
"ref": "8a51034d049c6a229d88dd62f490778a377eec06",
|
||||
"repo": "LSpec",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nix": {
|
||||
"inputs": {
|
||||
"lowdown-src": "lowdown-src",
|
||||
"nixpkgs": "nixpkgs",
|
||||
"nixpkgs-regression": "nixpkgs-regression"
|
||||
},
|
||||
"locked": {
|
||||
"lastModified": 1657097207,
|
||||
"narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nix",
|
||||
"rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nix",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1728500571,
|
||||
"narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=",
|
||||
"owner": "nixos",
|
||||
"lastModified": 1653988320,
|
||||
"narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0",
|
||||
"rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"ref": "nixos-24.05",
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-22.05-small",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-lib": {
|
||||
"locked": {
|
||||
"lastModified": 1730504152,
|
||||
"narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=",
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
|
||||
"dir": "lib",
|
||||
"lastModified": 1709237383,
|
||||
"narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
|
||||
"dir": "lib",
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-unstable",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-lib_2": {
|
||||
"nixpkgs-old": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1727825735,
|
||||
"narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
|
||||
"lastModified": 1581379743,
|
||||
"narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"type": "tarball",
|
||||
"url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
|
||||
"owner": "NixOS",
|
||||
"ref": "nixos-19.03",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-regression": {
|
||||
"locked": {
|
||||
"lastModified": 1643052045,
|
||||
"narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs_2": {
|
||||
"locked": {
|
||||
"lastModified": 1731386116,
|
||||
"narHash": "sha256-lKA770aUmjPHdTaJWnP3yQ9OI1TigenUqVC3wweqZuI=",
|
||||
"lastModified": 1686089707,
|
||||
"narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
|
||||
"owner": "NixOS",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "NixOS",
|
||||
"ref": "nixpkgs-unstable",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs_3": {
|
||||
"locked": {
|
||||
"lastModified": 1711703276,
|
||||
"narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "689fed12a013f56d4c4d3f612489634267d86529",
|
||||
"rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"ref": "nixos-24.05",
|
||||
"ref": "nixos-unstable",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
|
|
@ -131,9 +227,9 @@
|
|||
"root": {
|
||||
"inputs": {
|
||||
"flake-parts": "flake-parts",
|
||||
"lean4-nix": "lean4-nix",
|
||||
"lean": "lean",
|
||||
"lspec": "lspec",
|
||||
"nixpkgs": "nixpkgs_2"
|
||||
"nixpkgs": "nixpkgs_3"
|
||||
}
|
||||
}
|
||||
},
|
||||
|
|
|
|||
35
flake.nix
35
flake.nix
|
|
@ -2,11 +2,14 @@
|
|||
description = "Pantograph";
|
||||
|
||||
inputs = {
|
||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
|
||||
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
|
||||
flake-parts.url = "github:hercules-ci/flake-parts";
|
||||
lean4-nix.url = "github:lenianiva/lean4-nix";
|
||||
lean = {
|
||||
# Do not follow input's nixpkgs since it could cause build failures
|
||||
url = "github:leanprover/lean4?ref=v4.10.0-rc1";
|
||||
};
|
||||
lspec = {
|
||||
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
|
||||
url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
|
||||
flake = false;
|
||||
};
|
||||
};
|
||||
|
|
@ -15,7 +18,7 @@
|
|||
self,
|
||||
nixpkgs,
|
||||
flake-parts,
|
||||
lean4-nix,
|
||||
lean,
|
||||
lspec,
|
||||
...
|
||||
} : flake-parts.lib.mkFlake { inherit inputs; } {
|
||||
|
|
@ -26,16 +29,13 @@
|
|||
"x86_64-darwin"
|
||||
];
|
||||
perSystem = { system, pkgs, ... }: let
|
||||
pkgs = import nixpkgs {
|
||||
inherit system;
|
||||
overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
|
||||
};
|
||||
lspecLib = pkgs.lean.buildLeanPackage {
|
||||
leanPkgs = lean.packages.${system};
|
||||
lspecLib = leanPkgs.buildLeanPackage {
|
||||
name = "LSpec";
|
||||
roots = [ "Main" "LSpec" ];
|
||||
src = "${lspec}";
|
||||
};
|
||||
project = pkgs.lean.buildLeanPackage {
|
||||
project = leanPkgs.buildLeanPackage {
|
||||
name = "Pantograph";
|
||||
roots = [ "Pantograph" ];
|
||||
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
|
||||
|
|
@ -46,7 +46,7 @@
|
|||
!(pkgs.lib.hasSuffix "Repl.lean" path);
|
||||
});
|
||||
};
|
||||
repl = pkgs.lean.buildLeanPackage {
|
||||
repl = leanPkgs.buildLeanPackage {
|
||||
name = "Repl";
|
||||
roots = [ "Main" "Repl" ];
|
||||
deps = [ project ];
|
||||
|
|
@ -57,7 +57,7 @@
|
|||
!(pkgs.lib.hasSuffix ".md" path);
|
||||
});
|
||||
};
|
||||
test = pkgs.lean.buildLeanPackage {
|
||||
test = leanPkgs.buildLeanPackage {
|
||||
name = "Test";
|
||||
# NOTE: The src directory must be ./. since that is where the import
|
||||
# root begins (e.g. `import Test.Environment` and not `import
|
||||
|
|
@ -72,25 +72,24 @@
|
|||
};
|
||||
in rec {
|
||||
packages = {
|
||||
inherit (pkgs.lean) lean lean-all;
|
||||
inherit (project) sharedLib iTree;
|
||||
inherit (leanPkgs) lean lean-all;
|
||||
inherit (project) sharedLib;
|
||||
inherit (repl) executable;
|
||||
default = repl.executable;
|
||||
};
|
||||
legacyPackages = {
|
||||
inherit project;
|
||||
leanPkgs = pkgs.lean;
|
||||
inherit project leanPkgs;
|
||||
};
|
||||
checks = {
|
||||
test = pkgs.runCommand "test" {
|
||||
buildInputs = [ test.executable pkgs.lean.lean-all ];
|
||||
buildInputs = [ test.executable leanPkgs.lean-all ];
|
||||
} ''
|
||||
#export LEAN_SRC_PATH="${./.}"
|
||||
${test.executable}/bin/test > $out
|
||||
'';
|
||||
};
|
||||
devShells.default = pkgs.mkShell {
|
||||
buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
|
||||
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
|
||||
};
|
||||
};
|
||||
};
|
||||
|
|
|
|||
|
|
@ -1,14 +1,13 @@
|
|||
{"version": "1.1.0",
|
||||
{"version": 7,
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages":
|
||||
[{"url": "https://github.com/lenianiva/LSpec.git",
|
||||
[{"url": "https://github.com/lurk-lab/LSpec.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
|
||||
"rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
|
||||
"name": "LSpec",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
|
||||
"inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
|
||||
"inherited": false,
|
||||
"configFile": "lakefile.lean"}],
|
||||
"name": "pantograph",
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ lean_exe repl {
|
|||
}
|
||||
|
||||
require LSpec from git
|
||||
"https://github.com/lenianiva/LSpec.git" @ "c492cecd0bc473e2f9c8b94d545d02cc0056034f"
|
||||
"https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
|
||||
lean_lib Test {
|
||||
}
|
||||
@[test_driver]
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.12.0
|
||||
leanprover/lean4:v4.10.0-rc1
|
||||
|
|
|
|||
Loading…
Reference in New Issue