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>.

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

Pantograph.lean

@@ -1,6 +1,6 @@
+import Pantograph.Compile
 import Pantograph.Condensed
 import Pantograph.Environment
-import Pantograph.Frontend
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol

Pantograph/Compile.lean

@@ -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

Pantograph/Compile/Elab.lean

@@ -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. -/
@@ -125,17 +121,17 @@ protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
 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
@@ -146,65 +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
-    return { goalBefore, goalAfter, tactic }
 
-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

Pantograph/Compile/Frontend.lean

@@ -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

Pantograph/Compile/Parse.lean

@@ -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

Pantograph/Condensed.lean

@@ -2,6 +2,7 @@
 import Lean
 import Pantograph.Goal
 import Pantograph.Expr
+import Pantograph.Protocol
 
 open Lean
 

Pantograph/Environment.lean

@@ -10,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)
 
@@ -24,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"

Pantograph/Expr.lean

@@ -1,5 +1,4 @@
 import Lean
-import Std.Data.HashMap
 
 open Lean
 
@@ -61,54 +60,53 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
       -- 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}"
+      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 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}"
+        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
-        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))
+        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
@@ -145,10 +143,10 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d
   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 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[fvarId]?
+    let a := fvarArgMap.find? fvarId
     return acc ++ [(fvarId, a)]
 
   assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)

Pantograph/Frontend.lean

@@ -1,4 +0,0 @@
-/- Adapted from lean-training-data by semorrison -/
-import Pantograph.Frontend.Basic
-import Pantograph.Frontend.Elab
-import Pantograph.Frontend.MetaTranslate

Pantograph/Frontend/MetaTranslate.lean

@@ -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

Pantograph/Goal.lean

@@ -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

Pantograph/Library.lean

@@ -159,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
@@ -167,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

Pantograph/Protocol.lean

@@ -219,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
@@ -285,32 +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
   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 α

Pantograph/Serial.lean

@@ -26,13 +26,6 @@ def parseTerm (env: Environment) (s: String): Except String Syntax :=
     (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

Pantograph/Version.lean

@@ -1,6 +1,6 @@
 namespace Pantograph
 
 @[export pantograph_version]
-def version := "0.2.19"
+def version := "0.2.18"
 
 end Pantograph

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
+```

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)
@@ -46,7 +46,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   | "goal.continue" => run goal_continue
   | "goal.delete"   => run goal_delete
   | "goal.print"    => run goal_print
-  | "frontend.process"  => run frontend_process
+  | "compile.unit"  => run compile_unit
   | cmd =>
     let error: Protocol.InteractionError :=
       errorCommand s!"Unknown command {cmd}"
@@ -54,19 +54,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   where
   errorCommand := errorI "command"
   errorIndex := errorI "index"
-  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
@@ -103,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 #[])
@@ -115,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
@@ -149,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,
@@ -174,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 =>
@@ -204,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

Test/Environment.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) =>

Test/Frontend.lean

@@ -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

Test/Integration.lean

@@ -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,71 +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: Prop), p → p := by\n  intro p h\n  exact h"
-    let goal1 := "p : Prop\nh : p\n⊢ p"
-    step "frontend.process"
-      [
-        ("file", .str file),
-        ("invocations", .bool true),
-        ("sorrys", .bool false),
-      ]
-     ({
-       units := [{
-         boundary := (0, file.utf8ByteSize),
-         invocations? := .some [
-           {
-             goalBefore := "⊢ ∀ (p : Prop), p → p",
-             goalAfter := goal1,
-             tactic := "intro p h",
-           },
-           {
-             goalBefore := goal1 ,
-             goalAfter := "",
-             tactic := "exact h",
-           },
-         ]
-       }],
-    }: 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 := {
@@ -247,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))
 

Test/Main.lean

@@ -1,6 +1,5 @@
 import LSpec
 import Test.Environment
-import Test.Frontend
 import Test.Integration
 import Test.Library
 import Test.Metavar
@@ -45,7 +44,6 @@ 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),

flake.lock

@@ -36,74 +36,111 @@
     "lean": {
       "inputs": {
         "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs",
-        "nixpkgs-cadical": "nixpkgs-cadical",
+        "lean4-mode": "lean4-mode",
+        "nix": "nix",
+        "nixpkgs": "nixpkgs_2",
         "nixpkgs-old": "nixpkgs-old"
       },
       "locked": {
-        "lastModified": 1727749878,
-        "narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=",
+        "lastModified": 1719788866,
+        "narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=",
         "owner": "leanprover",
         "repo": "lean4",
-        "rev": "dc2533473114eb8656439ff2b9335209784aa640",
+        "rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4",
         "type": "github"
       },
       "original": {
         "owner": "leanprover",
-        "ref": "v4.12.0",
+        "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": 1686089707,
-        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
+        "lastModified": 1653988320,
+        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
+        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
+        "ref": "nixos-22.05-small",
         "repo": "nixpkgs",
         "type": "github"
       }
     },
-    "nixpkgs-cadical": {
-      "locked": {
-        "lastModified": 1722221733,
-        "narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
-        "type": "github"
-      }
-    },
     "nixpkgs-lib": {
       "locked": {
         "dir": "lib",
@@ -139,7 +176,39 @@
         "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": 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=",
@@ -160,7 +229,7 @@
         "flake-parts": "flake-parts",
         "lean": "lean",
         "lspec": "lspec",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_3"
       }
     }
   },

flake.nix

@@ -6,10 +6,10 @@
     flake-parts.url = "github:hercules-ci/flake-parts";
     lean = {
       # Do not follow input's nixpkgs since it could cause build failures
-      url = "github:leanprover/lean4?ref=v4.12.0";
+      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;
     };
   };
@@ -29,7 +29,7 @@
       "x86_64-darwin"
     ];
     perSystem = { system, pkgs, ... }: let
-      leanPkgs = lean.packages.${system}.deprecated;
+      leanPkgs = lean.packages.${system};
       lspecLib = leanPkgs.buildLeanPackage {
         name = "LSpec";
         roots = [ "Main" "LSpec" ];

lake-manifest.json

@@ -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",

lakefile.lean

@@ -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]

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.10.0-rc1