34 changed files with 1652 additions and 1727 deletions
--- a/802
+++ b/802
@ -1,190 +1,674 @@
-                                 Apache License
+                    GNU GENERAL PUBLIC LICENSE
-                           Version 2.0, January 2004
+                       Version 3, 29 June 2007
                        http://www.apache.org/licenses/
-   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,
+  The GNU General Public License is a free, copyleft license for
-      and distribution as defined by Sections 1 through 9 of this document.
+software and other kinds of works.
-      "Licensor" shall mean the copyright owner or entity authorized by
+  The licenses for most software and other practical works are designed
-      the copyright owner that is granting the License.
+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
+  When we speak of free software, we are referring to freedom, not
-      other entities that control, are controlled by, or are under common
+price.  Our General Public Licenses are designed to make sure that you
-      control with that entity. For the purposes of this definition,
+have the freedom to distribute copies of free software (and charge for
-      "control" means (i) the power, direct or indirect, to cause the
+them if you wish), that you receive source code or can get it if you
-      direction or management of such entity, whether by contract or
+want it, that you can change the software or use pieces of it in new
-      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+free programs, and that you know you can do these things.
      outstanding shares, or (iii) beneficial ownership of such entity.
-      "You" (or "Your") shall mean an individual or Legal Entity
+  To protect your rights, we need to prevent others from denying you
-      exercising permissions granted by this License.
+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,
+  For example, if you distribute copies of such a program, whether
-      including but not limited to software source code, documentation
+gratis or for a fee, you must pass on to the recipients the same
-      source, and configuration files.
+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
+  Developers that use the GNU GPL protect your rights with two steps:
-      transformation or translation of a Source form, including but
+(1) assert copyright on the software, and (2) offer you this License
-      not limited to compiled object code, generated documentation,
+giving you legal permission to copy, distribute and/or modify it.
      and conversions to other media types.
-      "Work" shall mean the work of authorship, whether in Source or
+  For the developers' and authors' protection, the GPL clearly explains
-      Object form, made available under the License, as indicated by a
+that there is no warranty for this free software.  For both users' and
-      copyright notice that is included in or attached to the work
+authors' sake, the GPL requires that modified versions be marked as
-      (an example is provided in the Appendix below).
+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
+  Some devices are designed to deny users access to install or run
-      form, that is based on (or derived from) the Work and for which the
+modified versions of the software inside them, although the manufacturer
-      editorial revisions, annotations, elaborations, or other modifications
+can do so.  This is fundamentally incompatible with the aim of
-      represent, as a whole, an original work of authorship. For the purposes
+protecting users' freedom to change the software.  The systematic
-      of this License, Derivative Works shall not include works that remain
+pattern of such abuse occurs in the area of products for individuals to
-      separable from, or merely link (or bind by name) to the interfaces of,
+use, which is precisely where it is most unacceptable.  Therefore, we
-      the Work and Derivative Works thereof.
+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
+  Finally, every program is threatened constantly by software patents.
-      the original version of the Work and any modifications or additions
+States should not allow patents to restrict development and use of
-      to that Work or Derivative Works thereof, that is intentionally
+software on general-purpose computers, but in those that do, we wish to
-      submitted to Licensor for inclusion in the Work by the copyright owner
+avoid the special danger that patents applied to a free program could
-      or by an individual or Legal Entity authorized to submit on behalf of
+make it effectively proprietary.  To prevent this, the GPL assures that
-      the copyright owner. For the purposes of this definition, "submitted"
+patents cannot be used to render the program non-free.
      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."
-      "Contributor" shall mean Licensor and any individual or Legal Entity
+  The precise terms and conditions for copying, distribution and
-      on behalf of whom a Contribution has been received by Licensor and
+modification follow.
      subsequently incorporated within the Work.
-   2. Grant of Copyright License. Subject to the terms and conditions of
+                       TERMS AND CONDITIONS
      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.
-   3. Grant of Patent License. Subject to the terms and conditions of
+  0. Definitions.
      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.
-   4. Redistribution. You may reproduce and distribute copies of the
+  "This License" refers to version 3 of the GNU General Public License.
      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:
-      (a) You must give any other recipients of the Work or
+  "Copyright" also means copyright-like laws that apply to other kinds of
-          Derivative Works a copy of this License; and
+works, such as semiconductor masks.
-      (b) You must cause any modified files to carry prominent notices
+  "The Program" refers to any copyrightable work licensed under this
-          stating that You changed the files; and
+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
+  To "modify" a work means to copy from or adapt all or part of the work
-          that You distribute, all copyright, patent, trademark, and
+in a fashion requiring copyright permission, other than the making of an
-          attribution notices from the Source form of the Work,
+exact copy.  The resulting work is called a "modified version" of the
-          excluding those notices that do not pertain to any part of
+earlier work or a work "based on" the earlier work.
          the Derivative Works; and
-      (d) If the Work includes a "NOTICE" text file as part of its
+  A "covered work" means either the unmodified Program or a work based
-          distribution, then any Derivative Works that You distribute must
+on the Program.
          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.
-      You may add Your own copyright statement to Your modifications and
+  To "propagate" a work means to do anything with it that, without
-      may provide additional or different license terms and conditions
+permission, would make you directly or secondarily liable for
-      for use, reproduction, or distribution of Your modifications, or
+infringement under applicable copyright law, except executing it on a
-      for any such Derivative Works as a whole, provided Your use,
+computer or modifying a private copy.  Propagation includes copying,
-      reproduction, and distribution of the Work otherwise complies with
+distribution (with or without modification), making available to the
-      the conditions stated in this License.
+public, and in some countries other activities as well.
-   5. Submission of Contributions. Unless You explicitly state otherwise,
+  To "convey" a work means any kind of propagation that enables other
-      any Contribution intentionally submitted for inclusion in the Work
+parties to make or receive copies.  Mere interaction with a user through
-      by You to the Licensor shall be under the terms and conditions of
+a computer network, with no transfer of a copy, is not conveying.
      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.
-   6. Trademarks. This License does not grant permission to use the trade
+  An interactive user interface displays "Appropriate Legal Notices"
-      names, trademarks, service marks, or product names of the Licensor,
+to the extent that it includes a convenient and prominently visible
-      except as required for reasonable and customary use in describing the
+feature that (1) displays an appropriate copyright notice, and (2)
-      origin of the Work and reproducing the content of the NOTICE file.
+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
+  1. Source Code.
      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.
-   8. Limitation of Liability. In no event and under no legal theory,
+  The "source code" for a work means the preferred form of the work
-      whether in tort (including negligence), contract, or otherwise,
+for making modifications to it.  "Object code" means any non-source
-      unless required by applicable law (such as deliberate and grossly
+form of a work.
      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.
-   9. Accepting Warranty or Additional Liability. While redistributing
+  A "Standard Interface" means an interface that either is an official
-      the Work or Derivative Works thereof, You may choose to offer,
+standard defined by a recognized standards body, or, in the case of
-      and charge a fee for, acceptance of support, warranty, indemnity,
+interfaces specified for a particular programming language, one that
-      or other liability obligations and/or rights consistent with this
+is widely used among developers working in that language.
-      License. However, in accepting such obligations, You may act only
+
-      on Your own behalf and on Your sole responsibility, not on behalf
+  The "System Libraries" of an executable work include anything, other
-      of any other Contributor, and only if You agree to indemnify,
+than the work as a whole, that (a) is included in the normal form of
-      defend, and hold each Contributor harmless for any liability
+packaging a Major Component, but which is not part of that Major
-      incurred by, or claims asserted against, such Contributor by reason
+Component, and (b) serves only to enable use of the work with that
-      of your accepting any such warranty or additional liability.
+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.
  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.
  The Corresponding Source need not include anything that users
 can regenerate automatically from other parts of the Corresponding
 Source.
  The Corresponding Source for a work in source code form is that
 same work.
  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
-   Copyright 2024 Leni Aniva
+            How to Apply These Terms to Your New Programs
-   Licensed under the Apache License, Version 2.0 (the "License");
+  If you develop a new program, and you want it to be of the greatest
-   you may not use this file except in compliance with the License.
+possible use to the public, the best way to achieve this is to make it
-   You may obtain a copy of the License at
+free software which everyone can redistribute and change under these terms.
-       http://www.apache.org/licenses/LICENSE-2.0
+  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.
-   Unless required by applicable law or agreed to in writing, software
+    <one line to give the program's name and a brief idea of what it does.>
-   distributed under the License is distributed on an "AS IS" BASIS,
+    Copyright (C) <year>  <name of author>
-   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+
-   See the License for the specific language governing permissions and
+    This program is free software: you can redistribute it and/or modify
-   limitations under the License.
+    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>.
--- a/Main.lean
+++ b/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
 open Pantograph.Protocol
 /-- 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
  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
+    IO.println "Uncaught IO exception"
-    let error  := Lean.toJson ({ error := "io", desc := message }: InteractionError)
+    IO.println ex.toString
    IO.println error.compress
--- a/Pantograph.lean
+++ b/Pantograph.lean
@ -1,7 +1,6 @@
-import Pantograph.Delate
+import Pantograph.Compile
-import Pantograph.Elab
+import Pantograph.Condensed
 import Pantograph.Environment
 import Pantograph.Frontend
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
--- a/Pantograph/Compile.lean
+++ b/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
--- a/Pantograph/Frontend/Elab.lean
+++ b/Pantograph/Frontend/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.Compile.Frontend
 import Pantograph.Frontend.MetaTranslate
 import Pantograph.Goal
 import Pantograph.Protocol
 open Lean
@ -78,7 +75,7 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
 end Lean.Elab.InfoTree
-namespace Pantograph.Frontend
+namespace Pantograph.Compile
 -- Info tree filtering functions
@ -89,7 +86,6 @@ structure TacticInvocation where
 namespace TacticInvocation
 /-- Return the range of the tactic, as a pair of file positions. -/
@[export pantograph_frontend_tactic_invocation_range]
 protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx
 /-- Pretty print a tactic. -/
@ -122,27 +118,20 @@ protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
 protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
  t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
 protected def usedConstants (t: TacticInvocation) : NameSet :=
  let info := t.info
  info.goalsBefore
    |>.filterMap info.mctxAfter.getExprAssignmentCore?
    |>.map Expr.getUsedConstantsAsSet
    |>.foldl .union .empty
 end TacticInvocation
 /-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
-partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
+partial def findAllInfo (t : Elab.InfoTree) (ctx : Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
    List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
  match t with
-  | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
+  | .context inner t => findAllInfo t (inner.mergeIntoOuter? ctx) pred
  | .node i children  =>
-      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+      (if pred i then [(i, ctx, children)] else []) ++ children.toList.bind (fun t => findAllInfo t ctx pred)
  | _ => []
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
 each equipped with its relevant `ContextInfo`, and any children info trees. -/
-private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
+def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
  let infos := findAllInfo t none fun i => match i with
    | .ofTacticInfo _ => true
    | _ => false
@ -153,71 +142,5 @@ private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
 def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
  collectTacticNodes t |>.filter fun i => i.info.isSubstantive
@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
 def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
    | info@(.ofTacticInfo _) => info.isOriginal
    | _ => false
  let tactics := tacticInfoTrees.bind collectTactics
  tactics.mapM λ invocation => do
    let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
    let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
    let tactic ← invocation.ctx.runMetaM {} do
      let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
      return t.pretty
    let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
    return {
      goalBefore,
      goalAfter,
      tactic,
      usedConstants,
    }
-structure InfoWithContext where
+end Pantograph.Compile
  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
--- a/Pantograph/Compile/Frontend.lean
+++ b/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
+namespace Pantograph.Compile
 abbrev FrontendM := Elab.Frontend.FrontendM
 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: Elab.Frontend.FrontendM (CompilationStep × Bool) := do
 def processOneCommand: 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 [cmd]
      return []
  else
-      return [← f cmd]
+    return cmd :: (← processFile)
  else
    return (← f cmd) :: (← mapCompilationSteps f)
@[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"
-/--
+def processSource (module : Name) (opts : Options := {}) : IO (List CompilationStep) := unsafe do
-Use with
+  let file ← IO.FS.readFile (← findSourcePath module)
-```lean
+  let inputCtx := Parser.mkInputContext file module.toString
 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
  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 commandState := Elab.Command.mkState env messages opts
-  let context: Elab.Frontend.Context := { inputCtx }
+  processFile.run { inputCtx }
-  let state: Elab.Frontend.State := {
+    |>.run' {
    commandState := { commandState with infoState.enabled := true },
    parserState,
    cmdPos := parserState.pos
  }
  return (context, state)
-end Pantograph.Frontend
+
 end Pantograph.Compile
--- a/Pantograph/Compile/Parse.lean
+++ b/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
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@ -0,0 +1,96 @@
 /- structures for FFI based interface -/
 import Lean
 import Pantograph.Goal
 import Pantograph.Expr
 import Pantograph.Protocol
 open Lean
 namespace Pantograph
 namespace Condensed
 -- Mirrors Lean's LocalDecl
 structure LocalDecl where
  -- Default value is for testing
  fvarId: FVarId := { name := .anonymous }
  userName: Name
  -- Normalized expression
  type : Expr
  value? : Option Expr := .none
 structure Goal where
  mvarId: MVarId := { name := .anonymous }
  userName: Name := .anonymous
  context: Array LocalDecl
  target: Expr
@[export pantograph_goal_is_lhs]
 def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
 -- Functions for creating contexts and states
@[export pantograph_elab_context]
 def elabContext: Elab.Term.Context := {
    errToSorry := false
  }
 end Condensed
 -- Get the list of visible (by default) free variables from a goal
@[export pantograph_visible_fvars_of_mvar]
 protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
  let mvarDecl ← mctx.findDecl? mvarId
  let lctx := mvarDecl.lctx
  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
    | none      => r
@[export pantograph_to_condensed_goal_m]
 def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
  let ppAuxDecls     := Meta.pp.auxDecls.get (← getOptions)
  let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
  let mvarDecl ← mvarId.getDecl
  let lctx     := mvarDecl.lctx
  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
  Meta.withLCtx lctx mvarDecl.localInstances do
    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
      match localDecl with
      | .cdecl _ fvarId userName type _ _ =>
        let type ← instantiate type
        return { fvarId, userName, type }
      | .ldecl _ fvarId userName type value _ _ => do
        let userName := userName.simpMacroScopes
        let type ← instantiate type
        let value ← instantiate value
        return { fvarId, userName, type, value? := .some value }
    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
        !ppImplDetailHyps && localDecl.isImplementationDetail
      if skip then
        return acc
      else
        let var ← ppVar localDecl
        return var::acc
    return {
        mvarId,
        userName := mvarDecl.userName,
        context := vars.reverse.toArray,
        target := ← instantiate mvarDecl.type
    }
  where
  instantiate := instantiateAll
@[export pantograph_goal_state_to_condensed_m]
 protected def GoalState.toCondensed (state: GoalState):
    CoreM (Array Condensed.Goal):= do
  let metaM := do
    let goals := state.goals.toArray
    goals.mapM fun goal => do
      match state.mctx.findDecl? goal with
      | .some _ =>
        let serializedGoal ← toCondensedGoal goal
        pure serializedGoal
      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
  metaM.run' (s := state.savedState.term.meta.meta)
 end Pantograph
--- a/Pantograph/Delate.lean
+++ b/Pantograph/Delate.lean
@ -1,562 +0,0 @@
 /-
 This file handles "Delation": The conversion of Kernel view into Search view.
 -/
 import Lean
 import Std.Data.HashMap
 import Pantograph.Goal
 import Pantograph.Protocol
 open Lean
 -- Symbol processing functions --
 namespace Pantograph
 structure ProjectionApplication where
  projector: Name
  numParams: Nat
  inner: Expr
@[export pantograph_expr_proj_to_app]
 def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
  let (typeName, idx, inner) := match e with
    | .proj typeName idx inner => (typeName, idx, inner)
    | _ => panic! "Argument must be proj"
  let ctor := getStructureCtor env typeName
  let fieldName := getStructureFields env typeName |>.get! idx
  let projector := getProjFnForField? env typeName fieldName |>.get!
  {
    projector,
    numParams := ctor.numParams,
    inner,
  }
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
@[export pantograph_unfold_aux_lemmas]
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 /--
 Force the instantiation of delayed metavariables even if they cannot be fully
 instantiated. This is used during resumption to provide diagnostic data about
 the current goal.
 Since Lean 4 does not have an `Expr` constructor corresponding to delayed
 metavariables, any delayed metavariables must be recursively handled by this
 function to ensure that nested delayed metavariables can be properly processed.
 The caveat is this recursive call will lead to infinite recursion if a loop
 between metavariable assignment exists.
 This function ensures any metavariable in the result is either
 1. Delayed assigned with its pending mvar not assigned in any form
 2. Not assigned (delay or not)
 -/
 partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
  --let padding := String.join $ List.replicate level "│ "
  --IO.println s!"{padding}Starting {toString eOrig}"
  let mut result ← Meta.transform (← instantiateMVars eOrig)
    (pre := fun e => e.withApp fun f args => do
      let .mvar mvarId := f | return .continue
      --IO.println s!"{padding}├V {e}"
      let mvarDecl ← mvarId.getDecl
      -- This is critical to maintaining the interdependency of metavariables.
      -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
      -- system will not make the necessary delayed assigned mvars in case of
      -- nested mvars.
      mvarId.setKind .syntheticOpaque
      mvarId.withContext do
        let lctx ← MonadLCtx.getLCtx
        if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
          let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
            | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
            | .none => acc) []
          panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
        if let .some assign ← getExprMVarAssignment? mvarId then
          --IO.println s!"{padding}├A ?{mvarId.name}"
          assert! !(← mvarId.isDelayedAssigned)
          return .visit (mkAppN assign args)
        else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
          --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
          --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
          if args.size < fvars.size then
            throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
          --if !args.isEmpty then
            --IO.println s!"{padding}├── Arguments Begin"
          let args ← args.mapM self
          --if !args.isEmpty then
            --IO.println s!"{padding}├── Arguments End"
          if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
            --IO.println s!"{padding}├T1"
            let result := mkAppN f args
            return .done result
          let pending ← mvarIdPending.withContext do
            let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
            --IO.println s!"{padding}├Pre: {inner}"
            pure <| (← inner.abstractM fvars).instantiateRev args
          -- Tail arguments
          let result := mkAppRange pending fvars.size args.size args
          --IO.println s!"{padding}├MD {result}"
          return .done result
        else
          assert! !(← mvarId.isAssigned)
          assert! !(← mvarId.isDelayedAssigned)
          --if !args.isEmpty then
          --  IO.println s!"{padding}├── Arguments Begin"
          let args ← args.mapM self
          --if !args.isEmpty then
          --  IO.println s!"{padding}├── Arguments End"
          --IO.println s!"{padding}├M ?{mvarId.name}"
          return .done (mkAppN f args))
  --IO.println s!"{padding}└Result {result}"
  return result
  where
  self e := instantiateDelayedMVars e --(level := level + 1)
 /--
 Convert an expression to an equiavlent form with
 1. No nested delayed assigned mvars
 2. No aux lemmas
 3. No assigned mvars
 -/
@[export pantograph_instantiate_all_m]
 def instantiateAll (e: Expr): MetaM Expr := do
  let e ← instantiateDelayedMVars e
  let e ← unfoldAuxLemmas e
  return e
 structure DelayedMVarInvocation where
  mvarIdPending: MVarId
  args: Array (FVarId × (Option Expr))
  -- Extra arguments applied to the result of this substitution
  tail: Array Expr
 -- The pending mvar of any delayed assigned mvar must not be assigned in any way.
@[export pantograph_to_delayed_mvar_invocation_m]
 def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
  let .mvar mvarId := e.getAppFn | return .none
  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
  let mvarIdPending := decl.mvarIdPending
  let mvarDecl ← mvarIdPending.getDecl
  -- Print the function application e. See Lean's `withOverApp`
  let args := e.getAppArgs
  assert! args.size ≥ decl.fvars.size
  assert! !(← mvarIdPending.isAssigned)
  assert! !(← mvarIdPending.isDelayedAssigned)
  let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
  let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
    let fvarId := localDecl.fvarId
    let a := fvarArgMap[fvarId]?
    return acc ++ [(fvarId, a)]
  assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
  return .some {
    mvarIdPending,
    args := subst.toArray,
    tail := args.toList.drop decl.fvars.size |>.toArray,
  }
 -- Condensed representation
 namespace Condensed
 -- Mirrors Lean's LocalDecl
 structure LocalDecl where
  -- Default value is for testing
  fvarId: FVarId := { name := .anonymous }
  userName: Name
  -- Normalized expression
  type : Expr
  value? : Option Expr := .none
 structure Goal where
  mvarId: MVarId := { name := .anonymous }
  userName: Name := .anonymous
  context: Array LocalDecl
  target: Expr
@[export pantograph_goal_is_lhs]
 def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
 end Condensed
 -- Get the list of visible (by default) free variables from a goal
@[export pantograph_visible_fvars_of_mvar]
 protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
  let mvarDecl ← mctx.findDecl? mvarId
  let lctx := mvarDecl.lctx
  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
    | none      => r
@[export pantograph_to_condensed_goal_m]
 def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
  let ppAuxDecls     := Meta.pp.auxDecls.get (← getOptions)
  let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
  let mvarDecl ← mvarId.getDecl
  let lctx     := mvarDecl.lctx
  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
  Meta.withLCtx lctx mvarDecl.localInstances do
    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
      match localDecl with
      | .cdecl _ fvarId userName type _ _ =>
        let type ← instantiate type
        return { fvarId, userName, type }
      | .ldecl _ fvarId userName type value _ _ => do
        let userName := userName.simpMacroScopes
        let type ← instantiate type
        let value ← instantiate value
        return { fvarId, userName, type, value? := .some value }
    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
        !ppImplDetailHyps && localDecl.isImplementationDetail
      if skip then
        return acc
      else
        let var ← ppVar localDecl
        return var::acc
    return {
        mvarId,
        userName := mvarDecl.userName,
        context := vars.reverse.toArray,
        target := ← instantiate mvarDecl.type
    }
  where
  instantiate := instantiateAll
@[export pantograph_goal_state_to_condensed_m]
 protected def GoalState.toCondensed (state: GoalState):
    CoreM (Array Condensed.Goal):= do
  let metaM := do
    let goals := state.goals.toArray
    goals.mapM fun goal => do
      match state.mctx.findDecl? goal with
      | .some _ =>
        let serializedGoal ← toCondensedGoal goal
        pure serializedGoal
      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
  metaM.run' (s := state.savedState.term.meta.meta)
 def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
  Meta.forallTelescope expr fun arr body => do
    let binders ← arr.mapM fun fvar => do
      return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
    return { binders, target := toString (← Meta.ppExpr body) }
 def serializeName (name: Name) (sanitize: Bool := true): String :=
  let internal := name.isInaccessibleUserName || name.hasMacroScopes
  if sanitize && internal then "_"
  else toString name |> addQuotes
  where
  addQuotes (n: String) :=
    let quote := "\""
    if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
 partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
  let k := level.getOffset
  let u := level.getLevelOffset
  let u_str := match u with
    | .zero => "0"
    | .succ _ => panic! "getLevelOffset should not return .succ"
    | .max v w =>
      let v := serializeSortLevel v sanitize
      let w := serializeSortLevel w sanitize
      s!"(:max {v} {w})"
    | .imax v w =>
      let v := serializeSortLevel v sanitize
      let w := serializeSortLevel w sanitize
      s!"(:imax {v} {w})"
    | .param name =>
      let name := serializeName name sanitize
      s!"{name}"
    | .mvar id =>
      let name := serializeName id.name sanitize
      s!"(:mv {name})"
  match k, u with
  | 0, _ => u_str
  | _, .zero => s!"{k}"
  | _, _ => s!"(+ {u_str} {k})"
 /--
 Completely serializes an expression tree. Json not used due to compactness
 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
 partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
  self expr
  where
  delayedMVarToSexp (e: Expr): MetaM (Option String) := do
    let .some invocation ← toDelayedMVarInvocation e | return .none
    let callee ← self $ .mvar invocation.mvarIdPending
    let sites ← invocation.args.mapM (λ (fvarId, arg) => do
        let arg := match arg with
          | .some arg => arg
          | .none => .fvar fvarId
        self arg
      )
    let tailArgs ← invocation.tail.mapM self
    let sites := " ".intercalate sites.toList
    let result := if tailArgs.isEmpty then
        s!"(:subst {callee} {sites})"
      else
        let tailArgs := " ".intercalate tailArgs.toList
        s!"((:subst {callee} {sites}) {tailArgs})"
    return .some result
  self (e: Expr): MetaM String := do
    if let .some result ← delayedMVarToSexp e then
      return result
    match e with
    | .bvar deBruijnIndex =>
      -- This is very common so the index alone is shown. Literals are handled below.
      -- The raw de Bruijn index should never appear in an unbound setting. In
      -- Lean these are handled using a `#` prefix.
      pure s!"{deBruijnIndex}"
    | .fvar fvarId =>
      let name := ofName fvarId.name
      pure s!"(:fv {name})"
    | .mvar mvarId => do
        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
        let name := ofName mvarId.name
        pure s!"(:{pref} {name})"
    | .sort level =>
      let level := serializeSortLevel level sanitize
      pure s!"(:sort {level})"
    | .const declName _ =>
      -- The universe level of the const expression is elided since it should be
      -- inferrable from surrounding expression
      pure s!"(:c {declName})"
    | .app _ _ => do
      let fn' ← self e.getAppFn
      let args := (← e.getAppArgs.mapM self) |>.toList
      let args := " ".intercalate args
      pure s!"({fn'} {args})"
    | .lam binderName binderType body binderInfo => do
      let binderName' := ofName binderName
      let binderType' ← self binderType
      let body' ← self body
      let binderInfo' := binderInfoSexp binderInfo
      pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
    | .forallE binderName binderType body binderInfo => do
      let binderName' := ofName binderName
      let binderType' ← self binderType
      let body' ← self body
      let binderInfo' := binderInfoSexp binderInfo
      pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
    | .letE name type value body _ => do
      -- Dependent boolean flag diacarded
      let name' := serializeName name
      let type' ← self type
      let value' ← self value
      let body' ← self body
      pure s!"(:let {name'} {type'} {value'} {body'})"
    | .lit v =>
      -- To not burden the downstream parser who needs to handle this, the literal
      -- is wrapped in a :lit sexp.
      let v' := match v with
        | .natVal val => toString val
        | .strVal val => s!"\"{val}\""
      pure s!"(:lit {v'})"
    | .mdata _ inner =>
      -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
      -- It may become necessary to incorporate the metadata.
      self inner
    | .proj _ _ _ => do
      let env ← getEnv
      let projApp := exprProjToApp env e
      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
      let inner ← self projApp.inner
      pure s!"((:c {projApp.projector}) {autos} {inner})"
  -- Elides all unhygenic names
  binderInfoSexp : Lean.BinderInfo → String
    | .default => ""
    | .implicit => " :implicit"
    | .strictImplicit => " :strictImplicit"
    | .instImplicit => " :instImplicit"
  ofName (name: Name) := serializeName name sanitize
 def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
  let pp?: Option String ← match options.printExprPretty with
    | true => pure $ .some $ toString $ ← Meta.ppExpr e
    | false => pure $ .none
  let sexp?: Option String ← match options.printExprAST with
    | true => pure $ .some $ ← serializeExpressionSexp e
    | false => pure $ .none
  let dependentMVars? ← match options.printDependentMVars with
    | true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
    | false => pure $ .none
  return {
    pp?,
    sexp?
    dependentMVars?,
  }
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
      : MetaM Protocol.Goal := do
  -- Options for printing; See Meta.ppGoal for details
  let showLetValues  := true
  let ppAuxDecls     := options.printAuxDecls
  let ppImplDetailHyps := options.printImplementationDetailHyps
  let lctx           := mvarDecl.lctx
  let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
  Meta.withLCtx lctx mvarDecl.localInstances do
    let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
      match localDecl with
      | .cdecl _ fvarId userName _ _ _ =>
        return {
          name := ofName fvarId.name,
          userName:= ofName userName.simpMacroScopes,
          isInaccessible := userName.isInaccessibleUserName
        }
      | .ldecl _ fvarId userName _ _ _ _ => do
        return {
          name := ofName fvarId.name,
          userName := toString userName.simpMacroScopes,
          isInaccessible := userName.isInaccessibleUserName
        }
    let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
      match localDecl with
      | .cdecl _ fvarId userName type _ _ =>
        let userName := userName.simpMacroScopes
        let type ← instantiate type
        return {
          name := ofName fvarId.name,
          userName:= ofName userName,
          isInaccessible := userName.isInaccessibleUserName
          type? := .some (← serializeExpression options type)
        }
      | .ldecl _ fvarId userName type val _ _ => do
        let userName := userName.simpMacroScopes
        let type ← instantiate type
        let value? ← if showLetValues then
          let val ← instantiate val
          pure $ .some (← serializeExpression options val)
        else
          pure $ .none
        return {
          name := ofName fvarId.name,
          userName:= ofName userName,
          isInaccessible := userName.isInaccessibleUserName
          type? := .some (← serializeExpression options type)
          value? := value?
        }
    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
        !ppImplDetailHyps && localDecl.isImplementationDetail
      if skip then
        return acc
      else
        let nameOnly := options.noRepeat && (parentDecl?.map
          (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
        let var ← match nameOnly with
          | true => ppVarNameOnly localDecl
          | false => ppVar localDecl
        return var::acc
    return {
      name := ofName goal.name,
      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
      target := (← serializeExpression options (← instantiate mvarDecl.type)),
      vars := vars.reverse.toArray
    }
  where
  instantiate := instantiateAll
  ofName (n: Name) := serializeName n (sanitize := false)
 protected def GoalState.serializeGoals
      (state: GoalState)
      (parent: Option GoalState := .none)
      (options: @&Protocol.Options := {}):
    MetaM (Array Protocol.Goal):= do
  state.restoreMetaM
  let goals := state.goals.toArray
  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
  goals.mapM fun goal => do
    match state.mctx.findDecl? goal with
    | .some mvarDecl =>
      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
      pure serializedGoal
    | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 /-- Print the metavariables in a readable format -/
@[export pantograph_goal_state_diag_m]
 protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
  let metaM: MetaM String := do
    goalState.restoreMetaM
    let savedState := goalState.savedState
    let goals := savedState.tactic.goals
    let mctx ← getMCtx
    let root := goalState.root
    -- Print the root
    let result: String ← match mctx.decls.find? root with
      | .some decl => printMVar ">" root decl
      | .none => pure s!">{root.name}: ??"
    let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
      match mctx.decls.find? mvarId with
      | .some decl => printMVar "⊢" mvarId decl
      | .none => pure s!"⊢{mvarId.name}: ??"
    )
    let goals := goals.toSSet
    let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
        !(goals.contains mvarId || mvarId == root) && options.printAll)
        |>.mapM (fun (mvarId, decl) => do
          let pref := if parentHasMVar mvarId then " " else "~"
          printMVar pref mvarId decl
        )
    pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
  metaM.run' {}
  where
    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
      let resultFVars: List String ←
        if options.printContext then
          decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
            do pure $ (← printFVar fvarId decl) ++ "\n")
        else
          pure []
      let type ← if options.instantiate
        then instantiateAll decl.type
        else pure $ decl.type
      let type_sexp ← if options.printSexp then
          let sexp ← serializeExpressionSexp type (sanitize := false)
          pure <| " " ++ sexp
        else
          pure ""
      let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
      let resultValue: String ←
        if options.printValue then
          if let .some value ← getExprMVarAssignment? mvarId then
            let value ← if options.instantiate
              then instantiateAll value
              else pure $ value
            pure s!"\n := {← Meta.ppExpr value}"
          else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
            pure s!"\n ::= {mvarIdPending.name}"
          else
            pure ""
        else
          pure ""
      pure $ (String.join resultFVars) ++ resultMain ++ resultValue
    printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
      pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
    userNameToString : Name → String
      | .anonymous => ""
      | other => s!"[{other}]"
    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 end Pantograph
--- a/Pantograph/Elab.lean
+++ b/Pantograph/Elab.lean
@ -1,40 +0,0 @@
 import Lean
 open Lean
 namespace Pantograph
 -- Functions for creating contexts and states
@[export pantograph_default_elab_context]
 def defaultElabContext: Elab.Term.Context := {
    errToSorry := false
  }
 /-- Read syntax object from string -/
 def parseTerm (env: Environment) (s: String): Except String Syntax :=
  Parser.runParserCategory
    (env := env)
    (catName := `term)
    (input := s)
    (fileName := "<stdin>")
 def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
  return Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := s)
    (fileName := "<stdin>")
 /-- Parse a syntax object. May generate additional metavariables! -/
 def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
  try
    let expr ← Elab.Term.elabType syn
    return .ok expr
  catch ex => return .error (← ex.toMessageData.toString)
 def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
  try
    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
    return .ok expr
  catch ex => return .error (← ex.toMessageData.toString)
 end Pantograph
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -1,9 +1,6 @@
 import Pantograph.Delate
 import Pantograph.Elab
 import Pantograph.Protocol
 import Pantograph.Serial
-import Lean.Environment
+import Lean
 import Lean.Replay
 open Lean
 open Pantograph
@ -13,12 +10,16 @@ namespace Pantograph.Environment
@[export pantograph_is_name_internal]
 def isNameInternal (n: Name): Bool :=
  -- Returns true if the name is an implementation detail which should not be shown to the user.
-  n.isAuxLemma ∨ n.hasMacroScopes
+  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
  where
  isLeanSymbol (name: Name): Bool := match name.getRoot with
    | .str _ name => name == "Lean"
    | _ => true
 /-- Catalog all the non-internal and safe names -/
@[export pantograph_environment_catalog]
-def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
+def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info =>
-  match isNameInternal name with
+  match isNameInternal name || info.isUnsafe with
  | false => acc.push name
  | true => acc)
@ -27,6 +28,14 @@ def module_of_name (env: Environment) (name: Name): Option Name := do
  let moduleId ←  env.getModuleIdxFor? name
  return env.allImportedModuleNames.get! moduleId.toNat
@[export pantograph_constant_info_is_unsafe_or_partial]
 def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
@[export pantograph_constant_info_type]
 def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type
@[export pantograph_constant_info_value]
 def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas
 def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
  let pref := match info with
  | .axiomInfo  _ => "a"
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@ -0,0 +1,160 @@
 import Lean
 open Lean
 namespace Pantograph
 structure ProjectionApplication where
  projector: Name
  numParams: Nat
  inner: Expr
@[export pantograph_expr_proj_to_app]
 def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
  let (typeName, idx, inner) := match e with
    | .proj typeName idx inner => (typeName, idx, inner)
    | _ => panic! "Argument must be proj"
  let ctor := getStructureCtor env typeName
  let fieldName := getStructureFields env typeName |>.get! idx
  let projector := getProjFnForField? env typeName fieldName |>.get!
  {
    projector,
    numParams := ctor.numParams,
    inner,
  }
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
@[export pantograph_unfold_aux_lemmas]
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 /--
 Force the instantiation of delayed metavariables even if they cannot be fully
 instantiated. This is used during resumption to provide diagnostic data about
 the current goal.
 Since Lean 4 does not have an `Expr` constructor corresponding to delayed
 metavariables, any delayed metavariables must be recursively handled by this
 function to ensure that nested delayed metavariables can be properly processed.
 The caveat is this recursive call will lead to infinite recursion if a loop
 between metavariable assignment exists.
 This function ensures any metavariable in the result is either
 1. Delayed assigned with its pending mvar not assigned in any form
 2. Not assigned (delay or not)
 -/
 partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
  --let padding := String.join $ List.replicate level "│ "
  --IO.println s!"{padding}Starting {toString eOrig}"
  let mut result ← Meta.transform (← instantiateMVars eOrig)
    (pre := fun e => e.withApp fun f args => do
      let .mvar mvarId := f | return .continue
      --IO.println s!"{padding}├V {e}"
      let mvarDecl ← mvarId.getDecl
      -- This is critical to maintaining the interdependency of metavariables.
      -- Without setting `.syntheticOpaque`, Lean's metavariable elimination
      -- system will not make the necessary delayed assigned mvars in case of
      -- nested mvars.
      mvarId.setKind .syntheticOpaque
      let lctx ← MonadLCtx.getLCtx
      if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
        let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
          | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
          | .none => acc) []
        panic! s!"Local context variable violation: {violations}"
      if let .some assign ← getExprMVarAssignment? mvarId then
        --IO.println s!"{padding}├A ?{mvarId.name}"
        assert! !(← mvarId.isDelayedAssigned)
        return .visit (mkAppN assign args)
      else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
        --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
        --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
        if args.size < fvars.size then
          throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
        --if !args.isEmpty then
          --IO.println s!"{padding}├── Arguments Begin"
        let args ← args.mapM self
        --if !args.isEmpty then
          --IO.println s!"{padding}├── Arguments End"
        if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
          --IO.println s!"{padding}├T1"
          let result := mkAppN f args
          return .done result
        let pending ← mvarIdPending.withContext do
          let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
          --IO.println s!"{padding}├Pre: {inner}"
          pure <| (← inner.abstractM fvars).instantiateRev args
        -- Tail arguments
        let result := mkAppRange pending fvars.size args.size args
        --IO.println s!"{padding}├MD {result}"
        return .done result
      else
        assert! !(← mvarId.isAssigned)
        assert! !(← mvarId.isDelayedAssigned)
        --if !args.isEmpty then
        --  IO.println s!"{padding}├── Arguments Begin"
        let args ← args.mapM self
        --if !args.isEmpty then
        --  IO.println s!"{padding}├── Arguments End"
        --IO.println s!"{padding}├M ?{mvarId.name}"
        return .done (mkAppN f args))
  --IO.println s!"{padding}└Result {result}"
  return result
  where
  self e := instantiateDelayedMVars e --(level := level + 1)
 /--
 Convert an expression to an equiavlent form with
 1. No nested delayed assigned mvars
 2. No aux lemmas
 3. No assigned mvars
 -/
@[export pantograph_instantiate_all_m]
 def instantiateAll (e: Expr): MetaM Expr := do
  let e ← instantiateDelayedMVars e
  let e ← unfoldAuxLemmas e
  return e
 structure DelayedMVarInvocation where
  mvarIdPending: MVarId
  args: Array (FVarId × (Option Expr))
  -- Extra arguments applied to the result of this substitution
  tail: Array Expr
 -- The pending mvar of any delayed assigned mvar must not be assigned in any way.
@[export pantograph_to_delayed_mvar_invocation_m]
 def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
  let .mvar mvarId := e.getAppFn | return .none
  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
  let mvarIdPending := decl.mvarIdPending
  let mvarDecl ← mvarIdPending.getDecl
  -- Print the function application e. See Lean's `withOverApp`
  let args := e.getAppArgs
  assert! args.size ≥ decl.fvars.size
  assert! !(← mvarIdPending.isAssigned)
  assert! !(← mvarIdPending.isDelayedAssigned)
  let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
  let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
    let fvarId := localDecl.fvarId
    let a := fvarArgMap.find? fvarId
    return acc ++ [(fvarId, a)]
  assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
  return .some {
    mvarIdPending,
    args := subst.toArray,
    tail := args.toList.drop decl.fvars.size |>.toArray,
  }
 end Pantograph
--- a/Pantograph/Frontend.lean
+++ b/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
--- a/Pantograph/Frontend/MetaTranslate.lean
+++ b/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
--- a/Pantograph/Goal.lean
+++ b/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
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -1,7 +1,8 @@
 import Pantograph.Condensed
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
-import Pantograph.Delate
+import Pantograph.Serial
 import Pantograph.Version
 import Lean
@ -41,7 +42,7 @@ namespace Pantograph
 def runMetaM { α } (metaM: MetaM α): CoreM α :=
  metaM.run'
 def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := defaultElabContext) |>.run'
+  termElabM.run' (ctx := Condensed.elabContext) |>.run'
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
@ -158,7 +159,7 @@ def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticRes
  runTermElabM <| state.tryAssign goal expr
@[export pantograph_goal_have_m]
 protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
-  let type ← match (← parseTermM type) with
+  let type ← match (← Compile.parseTermM type) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  runTermElabM do
@ -166,28 +167,12 @@ protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: S
    state.tryTacticM goal $ Tactic.evalHave binderName.toName type
@[export pantograph_goal_try_define_m]
 protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
-  let expr ← match (← parseTermM expr) with
+  let expr ← match (← Compile.parseTermM expr) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  runTermElabM do
    state.restoreElabM
    state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
@[export pantograph_goal_try_motivated_apply_m]
 protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
  let recursor ← match (← parseTermM recursor) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
@[export pantograph_goal_try_no_confuse_m]
 protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
  let eq ← match (← parseTermM eq) with
    | .ok syn => pure syn
    | .error error => return .parseError error
  state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
@[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
  runTermElabM <| state.tryLet goal binderName type
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@ -183,12 +183,6 @@ structure EnvAdd where
 structure EnvAddResult where
  deriving Lean.ToJson
 structure EnvSaveLoad where
  path: System.FilePath
  deriving Lean.FromJson
 structure EnvSaveLoadResult where
  deriving Lean.ToJson
 /-- Set options; See `Options` struct above for meanings -/
 structure OptionsSet where
  printJsonPretty?: Option Bool
@ -225,7 +219,6 @@ structure GoalTactic where
  tactic?: Option String := .none
  expr?: Option String := .none
  have?: Option String := .none
  let?: Option String := .none
  calc?: Option String := .none
  -- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
  conv?: Option Bool := .none
@ -291,35 +284,21 @@ structure GoalDiag where
 /-- Executes the Lean compiler on a single file -/
-structure FrontendProcess where
+structure CompileUnit where
-  -- One of these two must be supplied: Either supply the file name or the content.
+  module: String
-  fileName?: Option String := .none
+  -- If set to true, query the string boundaries of compilation units
-  file?: Option String := .none
+  compilationUnits: Bool := false
  -- If set to true, collect tactic invocations
  invocations: Bool := false
  -- If set to true, collect `sorry`s
  sorrys: Bool := false
  deriving Lean.FromJson
 structure InvokedTactic where
  goalBefore: String
  goalAfter: String
  tactic: String
  -- List of used constants
  usedConstants: Array String
  deriving Lean.ToJson
-
+structure CompileUnitResult where
-structure CompilationUnit where
+  units?: Option $ List (Nat × Nat)
-  -- String boundaries of compilation units
+  invocations?: Option $ List InvokedTactic
  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
  deriving Lean.ToJson
 abbrev CR α := Except InteractionError α
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -1,73 +1,355 @@
-import Lean.Environment
+/-
-import Lean.Replay
+All serialisation functions;
-import Init.System.IOError
+This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
-import Std.Data.HashMap
+using `Scope`s.
 /-!
 Input/Output functions
 # Pickling and unpickling objects
 By abusing `saveModuleData` and `readModuleData` we can pickle and unpickle objects to disk.
 -/
 import Lean
 import Pantograph.Condensed
 import Pantograph.Expr
 import Pantograph.Goal
 import Pantograph.Protocol
 open Lean
 -- Symbol processing functions --
 namespace Pantograph
-/--
+
-Save an object to disk.
+--- Input Functions ---
-If you need to write multiple objects from within a single declaration,
+
-you will need to provide a unique `key` for each.
+/-- Read syntax object from string -/
-/
+def parseTerm (env: Environment) (s: String): Except String Syntax :=
-def pickle {α : Type} (path : System.FilePath) (x : α) (key : Name := by exact decl_name%) : IO Unit :=
+  Parser.runParserCategory
-  saveModuleData path key (unsafe unsafeCast x)
+    (env := env)
    (catName := `term)
    (input := s)
    (fileName := "<stdin>")
 /-- Parse a syntax object. May generate additional metavariables! -/
 def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
  try
    let expr ← Elab.Term.elabType syn
    return .ok expr
  catch ex => return .error (← ex.toMessageData.toString)
 def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
  try
    let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
    return .ok expr
  catch ex => return .error (← ex.toMessageData.toString)
 --- Output Functions ---
 def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
  Meta.forallTelescope expr fun arr body => do
    let binders ← arr.mapM fun fvar => do
      return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
    return { binders, target := toString (← Meta.ppExpr body) }
 def serializeName (name: Name) (sanitize: Bool := true): String :=
  let internal := name.isInaccessibleUserName || name.hasMacroScopes
  if sanitize && internal then "_"
  else toString name |> addQuotes
  where
  addQuotes (n: String) :=
    let quote := "\""
    if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
 partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
  let k := level.getOffset
  let u := level.getLevelOffset
  let u_str := match u with
    | .zero => "0"
    | .succ _ => panic! "getLevelOffset should not return .succ"
    | .max v w =>
      let v := serializeSortLevel v sanitize
      let w := serializeSortLevel w sanitize
      s!"(:max {v} {w})"
    | .imax v w =>
      let v := serializeSortLevel v sanitize
      let w := serializeSortLevel w sanitize
      s!"(:imax {v} {w})"
    | .param name =>
      let name := serializeName name sanitize
      s!"{name}"
    | .mvar id =>
      let name := serializeName id.name sanitize
      s!"(:mv {name})"
  match k, u with
  | 0, _ => u_str
  | _, .zero => s!"{k}"
  | _, _ => s!"(+ {u_str} {k})"
 /--
-Load an object from disk.
+ Completely serializes an expression tree. Json not used due to compactness
 Note: The returned `CompactedRegion` can be used to free the memory behind the value
 of type `α`, using `CompactedRegion.free` (which is only safe once all references to the `α` are
 released). Ignoring the `CompactedRegion` results in the data being leaked.
 Use `withUnpickle` to call `CompactedRegion.free` automatically.
-This function is unsafe because the data being loaded may not actually have type `α`, and this
+A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 may cause crashes or other bad behavior.
 -/
-unsafe def unpickle (α : Type) (path : System.FilePath) : IO (α × CompactedRegion) := do
+partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
-  let (x, region) ← readModuleData path
+  self expr
-  pure (unsafeCast x, region)
+  where
  delayedMVarToSexp (e: Expr): MetaM (Option String) := do
    let .some invocation ← toDelayedMVarInvocation e | return .none
    let callee ← self $ .mvar invocation.mvarIdPending
    let sites ← invocation.args.mapM (λ (fvarId, arg) => do
        let arg := match arg with
          | .some arg => arg
          | .none => .fvar fvarId
        self arg
      )
    let tailArgs ← invocation.tail.mapM self
-/-- Load an object from disk and run some continuation on it, freeing memory afterwards. -/
+    let sites := " ".intercalate sites.toList
-unsafe def withUnpickle [Monad m] [MonadLiftT IO m] {α β : Type}
+    let result := if tailArgs.isEmpty then
-    (path : System.FilePath) (f : α → m β) : m β := do
+        s!"(:subst {callee} {sites})"
-  let (x, region) ← unpickle α path
+      else
-  let r ← f x
+        let tailArgs := " ".intercalate tailArgs.toList
-  region.free
+        s!"((:subst {callee} {sites}) {tailArgs})"
-  pure r
+    return .some result
-/--
+  self (e: Expr): MetaM String := do
-Pickle an `Environment` to disk.
+    if let .some result ← delayedMVarToSexp e then
      return result
    match e with
    | .bvar deBruijnIndex =>
      -- This is very common so the index alone is shown. Literals are handled below.
      -- The raw de Bruijn index should never appear in an unbound setting. In
      -- Lean these are handled using a `#` prefix.
      pure s!"{deBruijnIndex}"
    | .fvar fvarId =>
      let name := ofName fvarId.name
      pure s!"(:fv {name})"
    | .mvar mvarId => do
        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
        let name := ofName mvarId.name
        pure s!"(:{pref} {name})"
    | .sort level =>
      let level := serializeSortLevel level sanitize
      pure s!"(:sort {level})"
    | .const declName _ =>
      -- The universe level of the const expression is elided since it should be
      -- inferrable from surrounding expression
      pure s!"(:c {declName})"
    | .app _ _ => do
      let fn' ← self e.getAppFn
      let args := (← e.getAppArgs.mapM self) |>.toList
      let args := " ".intercalate args
      pure s!"({fn'} {args})"
    | .lam binderName binderType body binderInfo => do
      let binderName' := ofName binderName
      let binderType' ← self binderType
      let body' ← self body
      let binderInfo' := binderInfoSexp binderInfo
      pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
    | .forallE binderName binderType body binderInfo => do
      let binderName' := ofName binderName
      let binderType' ← self binderType
      let body' ← self body
      let binderInfo' := binderInfoSexp binderInfo
      pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
    | .letE name type value body _ => do
      -- Dependent boolean flag diacarded
      let name' := serializeName name
      let type' ← self type
      let value' ← self value
      let body' ← self body
      pure s!"(:let {name'} {type'} {value'} {body'})"
    | .lit v =>
      -- To not burden the downstream parser who needs to handle this, the literal
      -- is wrapped in a :lit sexp.
      let v' := match v with
        | .natVal val => toString val
        | .strVal val => s!"\"{val}\""
      pure s!"(:lit {v'})"
    | .mdata _ inner =>
      -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
      -- It may become necessary to incorporate the metadata.
      self inner
    | .proj _ _ _ => do
      let env ← getEnv
      let projApp := exprProjToApp env e
      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
      let inner ← self projApp.inner
      pure s!"((:c {projApp.projector}) {autos} {inner})"
  -- Elides all unhygenic names
  binderInfoSexp : Lean.BinderInfo → String
    | .default => ""
    | .implicit => " :implicit"
    | .strictImplicit => " :strictImplicit"
    | .instImplicit => " :instImplicit"
  ofName (name: Name) := serializeName name sanitize
-We only store:
+def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
-* the list of imports
+  let pp?: Option String ← match options.printExprPretty with
-* the new constants from `Environment.constants`
+    | true => pure $ .some $ toString $ ← Meta.ppExpr e
-and when unpickling, we build a fresh `Environment` from the imports,
+    | false => pure $ .none
-and then add the new constants.
+  let sexp?: Option String ← match options.printExprAST with
-/
+    | true => pure $ .some $ ← serializeExpressionSexp e
-@[export pantograph_env_pickle_m]
+    | false => pure $ .none
-def env_pickle (env : Environment) (path : System.FilePath) : IO Unit :=
+  let dependentMVars? ← match options.printDependentMVars with
-  Pantograph.pickle path (env.header.imports, env.constants.map₂)
+    | true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
    | false => pure $ .none
  return {
    pp?,
    sexp?
    dependentMVars?,
  }
 /--
 Unpickle an `Environment` from disk.
-We construct a fresh `Environment` with the relevant imports,
+/-- Adapted from ppGoal -/
-and then replace the new constants.
+def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
-/
+      : MetaM Protocol.Goal := do
-@[export pantograph_env_unpickle_m]
+  -- Options for printing; See Meta.ppGoal for details
-def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do
+  let showLetValues  := true
-  let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path
+  let ppAuxDecls     := options.printAuxDecls
-  let env ← importModules imports {} 0
+  let ppImplDetailHyps := options.printImplementationDetailHyps
-  return (← env.replay (Std.HashMap.ofList map₂.toList), region)
+  let lctx           := mvarDecl.lctx
  let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
  Meta.withLCtx lctx mvarDecl.localInstances do
    let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
      match localDecl with
      | .cdecl _ fvarId userName _ _ _ =>
        return {
          name := ofName fvarId.name,
          userName:= ofName userName.simpMacroScopes,
          isInaccessible := userName.isInaccessibleUserName
        }
      | .ldecl _ fvarId userName _ _ _ _ => do
        return {
          name := ofName fvarId.name,
          userName := toString userName.simpMacroScopes,
          isInaccessible := userName.isInaccessibleUserName
        }
    let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
      match localDecl with
      | .cdecl _ fvarId userName type _ _ =>
        let userName := userName.simpMacroScopes
        let type ← instantiate type
        return {
          name := ofName fvarId.name,
          userName:= ofName userName,
          isInaccessible := userName.isInaccessibleUserName
          type? := .some (← serializeExpression options type)
        }
      | .ldecl _ fvarId userName type val _ _ => do
        let userName := userName.simpMacroScopes
        let type ← instantiate type
        let value? ← if showLetValues then
          let val ← instantiate val
          pure $ .some (← serializeExpression options val)
        else
          pure $ .none
        return {
          name := ofName fvarId.name,
          userName:= ofName userName,
          isInaccessible := userName.isInaccessibleUserName
          type? := .some (← serializeExpression options type)
          value? := value?
        }
    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
        !ppImplDetailHyps && localDecl.isImplementationDetail
      if skip then
        return acc
      else
        let nameOnly := options.noRepeat && (parentDecl?.map
          (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
        let var ← match nameOnly with
          | true => ppVarNameOnly localDecl
          | false => ppVar localDecl
        return var::acc
    return {
      name := ofName goal.name,
      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
      target := (← serializeExpression options (← instantiate mvarDecl.type)),
      vars := vars.reverse.toArray
    }
  where
  instantiate := instantiateAll
  ofName (n: Name) := serializeName n (sanitize := false)
 protected def GoalState.serializeGoals
      (state: GoalState)
      (parent: Option GoalState := .none)
      (options: @&Protocol.Options := {}):
    MetaM (Array Protocol.Goal):= do
  state.restoreMetaM
  let goals := state.goals.toArray
  let parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
  goals.mapM fun goal => do
    match state.mctx.findDecl? goal with
    | .some mvarDecl =>
      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
      pure serializedGoal
    | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 /-- Print the metavariables in a readable format -/
@[export pantograph_goal_state_diag_m]
 protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
  let metaM: MetaM String := do
    goalState.restoreMetaM
    let savedState := goalState.savedState
    let goals := savedState.tactic.goals
    let mctx ← getMCtx
    let root := goalState.root
    -- Print the root
    let result: String ← match mctx.decls.find? root with
      | .some decl => printMVar ">" root decl
      | .none => pure s!">{root.name}: ??"
    let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
      match mctx.decls.find? mvarId with
      | .some decl => printMVar "⊢" mvarId decl
      | .none => pure s!"⊢{mvarId.name}: ??"
    )
    let goals := goals.toSSet
    let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
        !(goals.contains mvarId || mvarId == root) && options.printAll)
        |>.mapM (fun (mvarId, decl) => do
          let pref := if parentHasMVar mvarId then " " else "~"
          printMVar pref mvarId decl
        )
    pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
  metaM.run' {}
  where
    printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
      let resultFVars: List String ←
        if options.printContext then
          decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
            do pure $ (← printFVar fvarId decl) ++ "\n")
        else
          pure []
      let type ← if options.instantiate
        then instantiateAll decl.type
        else pure $ decl.type
      let type_sexp ← if options.printSexp then
          let sexp ← serializeExpressionSexp type (sanitize := false)
          pure <| " " ++ sexp
        else
          pure ""
      let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
      let resultValue: String ←
        if options.printValue then
          if let .some value ← getExprMVarAssignment? mvarId then
            let value ← if options.instantiate
              then instantiateAll value
              else pure $ value
            pure s!"\n := {← Meta.ppExpr value}"
          else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
            pure s!"\n ::= {mvarIdPending.name}"
          else
            pure ""
        else
          pure ""
      pure $ (String.join resultFVars) ++ resultMain ++ resultValue
    printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
      pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
    userNameToString : Name → String
      | .anonymous => ""
      | other => s!"[{other}]"
    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 end Pantograph
--- a/Pantograph/Version.lean
+++ b/Pantograph/Version.lean
@ -1,6 +1,6 @@
 namespace Pantograph
@[export pantograph_version]
-def version := "0.2.19"
+def version := "0.2.18"
 end Pantograph
--- a/README.md
+++ b/README.md
@ -9,17 +9,30 @@ examine the symbol list of a Lean project for machine learning.
 ## Installation
-For Nix users, run
+For Nix based workflow, see below.
 ``` sh
 nix build .#{sharedLib,executable}
 ```
 to build either the shared library or executable.
 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
+Note that there isn't a 1-1 correspondence between executable (REPL) commands
-requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence
+and library functions.
 between executable (REPL) commands and library functions.
 Inject any project path via the `pantograph_init_search` function.
 ## 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
+The tests are based on `LSpec`. To run tests,
 ``` sh
 nix flake check
 ```
 or
 ``` 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
 ```
--- a/Repl.lean
+++ b/Repl.lean
@ -1,7 +1,7 @@
-import Std.Data.HashMap
+import Lean.Data.HashMap
 import Pantograph
-namespace Pantograph.Repl
+namespace Pantograph
 structure Context where
  imports: List String
@ -10,7 +10,7 @@ structure Context where
 structure State where
  options: Protocol.Options := {}
  nextId: Nat := 0
-  goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
+  goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
 /-- Main state monad for executing commands -/
 abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
@ -22,9 +22,8 @@ abbrev CR α := Except Protocol.InteractionError α
 def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
  metaM.run'
 def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
-  termElabM.run' (ctx := defaultElabContext) |>.run'
+  termElabM.run' (ctx := Condensed.elabContext) |>.run'
 /-- Main loop command of the REPL -/
 def execute (command: Protocol.Command): MainM Lean.Json := do
  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
    match Lean.fromJson? command.payload with
@ -33,7 +32,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
      | .ok result =>  return Lean.toJson result
      | .error ierror => return Lean.toJson ierror
    | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
  try
  match command.cmd with
  | "reset"         => run reset
  | "stat"          => run stat
@ -41,8 +39,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
  | "env.catalog"   => run env_catalog
  | "env.inspect"   => run env_inspect
  | "env.add"       => run env_add
    | "env.save"      => run env_save
    | "env.load"      => run env_load
  | "options.set"   => run options_set
  | "options.print" => run options_print
  | "goal.start"    => run goal_start
@ -50,31 +46,19 @@ 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}"
    return Lean.toJson error
  catch ex => do
    let error ← ex.toMessageData.toString
    return Lean.toJson $ errorIO error
  where
  errorCommand := errorI "command"
  errorIndex := errorI "index"
  errorIO := errorI "io"
  newGoalState (goalState: GoalState) : MainM Nat := do
    let state ← get
    let stateId := state.nextId
    set { state with
      goalStates := state.goalStates.insert stateId goalState,
      nextId := state.nextId + 1
    }
    return stateId
  -- Command Functions
  reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
    let state ← get
    let nGoals := state.goalStates.size
-    set { state with nextId := 0, goalStates := .empty }
+    set { state with nextId := 0, goalStates := Lean.HashMap.empty }
    return .ok { nGoals }
  stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
    let state ← get
@ -88,14 +72,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    Environment.inspect args state.options
  env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
    Environment.addDecl args
  env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
    let env ← Lean.MonadEnv.getEnv
    env_pickle env args.path
    return .ok {}
  env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do
    let (env, _) ← env_unpickle args.path
    Lean.setEnv env
    return .ok {}
  expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
    let state ← get
    exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
@ -119,6 +95,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
  options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
    return .ok (← get).options
  goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
    let state ← get
    let env ← Lean.MonadEnv.getEnv
    let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
      | .some expr, .none => goalStartExpr expr (args.levels.getD #[])
@ -131,33 +108,34 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    match expr? with
    | .error error => return .error error
    | .ok goalState =>
-      let stateId ← newGoalState goalState
+      let stateId := state.nextId
      set { state with
        goalStates := state.goalStates.insert stateId goalState,
        nextId := state.nextId + 1
      }
      return .ok { stateId, root := goalState.root.name.toString }
  goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
    let state ← get
-    let .some goalState := state.goalStates[args.stateId]? |
+    let .some goalState := state.goalStates.find? args.stateId |
      return .error $ errorIndex s!"Invalid state index {args.stateId}"
    let .some goal := goalState.goals.get? args.goalId |
      return .error $ errorIndex s!"Invalid goal index {args.goalId}"
    let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
-      match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv?  with
+      match args.tactic?, args.expr?, args.have?, args.calc?, args.conv?  with
-      | .some tactic, .none, .none, .none, .none, .none => do
+      | .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
+      | .none, .none, .none, .some pred, .none => do
        let binderName := args.binderName?.getD ""
        pure <| Except.ok <| ← goalState.tryLet goal binderName type
      | .none, .none, .none, .none, .some pred, .none => do
        pure <| Except.ok <| ← goalState.tryCalc goal pred
-      | .none, .none, .none, .none, .none, .some true => do
+      | .none, .none, .none, .none, .some true => do
        pure <| Except.ok <| ← goalState.conv goal
-      | .none, .none, .none, .none, .none, .some false => do
+      | .none, .none, .none, .none, .some false => do
        pure <| Except.ok <| ← goalState.convExit
-      | _, _, _, _, _, _ =>
+      | _, _, _, _, _ =>
        let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
        pure $ Except.error $ error
    match nextGoalState? with
@ -165,18 +143,19 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    | .ok (.success nextGoalState) => do
      let nextGoalState ← match state.options.automaticMode, args.conv? with
        | true, .none => do
-          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
+          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) | throwError "Resuming known goals"
            throwError "Resuming known goals"
          pure result
        | true, .some true => pure nextGoalState
        | true, .some false => do
-          let .some (_, _, dormantGoals) := goalState.convMVar? |
+          let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail"
-            throwError "If conv exit succeeded this should not fail"
+          let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals"
          let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
            throwError "Resuming known goals"
          pure result
        | false, _ => pure nextGoalState
-      let nextStateId ← newGoalState nextGoalState
+      let nextStateId := state.nextId
      set { state with
        goalStates := state.goalStates.insert state.nextId nextGoalState,
        nextId := state.nextId + 1,
      }
      let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
      return .ok {
        nextStateId? := .some nextStateId,
@ -190,11 +169,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
      return .ok { tacticErrors? := .some messages }
  goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
    let state ← get
-    let .some target := state.goalStates[args.target]? |
+    let .some target := state.goalStates.find? args.target | return .error $ errorIndex s!"Invalid state index {args.target}"
      return .error $ errorIndex s!"Invalid state index {args.target}"
    let nextState? ← match args.branch?, args.goals? with
      | .some branchId, .none => do
-        match state.goalStates[branchId]? with
+        match state.goalStates.find? branchId with
        | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
        | .some branch => pure $ target.continue branch
      | .none, .some goals =>
@ -220,57 +198,23 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
    return .ok {}
  goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
    let state ← get
-    let .some goalState := state.goalStates[args.stateId]? |
+    let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {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
+  compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
-    let options := (← get).options
+    let module := args.module.toName
    try
-      let (fileName, file) ← match args.fileName?, args.file? with
+      let steps ← Compile.processSource module
-        | .some fileName, .none => do
+      let units? := if args.compilationUnits then
-          let file ← IO.FS.readFile fileName
+          .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
-          pure (fileName, file)
+        else
-        | .none, .some file =>
+          .none
-          pure ("<anonymous>", file)
+      let invocations? ← if args.invocations then
-        | _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
+          pure $ .some (← Compile.collectTacticsFromCompilation steps)
      let env?: Option Lean.Environment ← if args.fileName?.isSome then
          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
+      return .ok { units?, invocations? }
            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 }
    catch e =>
-      return .error $ errorI "frontend" (← e.toMessageData.toString)
+      return .error $ errorI "compile" (← e.toMessageData.toString)
-end Pantograph.Repl
+end Pantograph
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -1,6 +1,7 @@
 import Pantograph.Goal
 import Pantograph.Library
 import Pantograph.Protocol
 import Pantograph.Condensed
 import Lean
 import LSpec
@ -89,9 +90,9 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
  runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := defaultElabContext)
+  termElabM.run' (ctx := Condensed.elabContext)
 def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
-  runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
+  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
--- a/Test/Environment.lean
+++ b/Test/Environment.lean
@ -1,5 +1,5 @@
 import LSpec
-import Pantograph.Delate
+import Pantograph.Serial
 import Pantograph.Environment
 import Test.Common
 import Lean
@ -33,7 +33,7 @@ def test_catalog: IO LSpec.TestSeq := do
 def test_symbol_visibility: IO LSpec.TestSeq := do
  let entries: List (Name × Bool) := [
    ("Nat.add_comm".toName, false),
-    ("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
+    ("Lean.Name".toName, true),
    ("Init.Data.Nat.Basic._auxLemma.4".toName, true),
  ]
  let suite := entries.foldl (λ suites (symbol, target) =>
--- a/Test/Frontend.lean
+++ b/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
--- a/Test/Integration.lean
+++ b/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,73 +161,6 @@ def test_env_add_inspect : Test :=
      Protocol.EnvInspectResult)
  ]
 example : ∀ (p: Prop), p → p := by
  intro p h
  exact h
 def test_frontend_process : Test :=
  [
    let file := "example : ∀ (p q: Prop), p → p ∨ q := by\n  intro p q h\n  exact Or.inl h"
    let goal1 := "p q : Prop\nh : p\n⊢ p ∨ q"
    step "frontend.process"
      [
        ("file", .str file),
        ("invocations", .bool true),
        ("sorrys", .bool false),
      ]
     ({
       units := [{
         boundary := (0, file.utf8ByteSize),
         invocations? := .some [
           {
             goalBefore := "⊢ ∀ (p q : Prop), p → p ∨ q",
             goalAfter := goal1,
             tactic := "intro p q h",
             usedConstants := #[],
           },
           {
             goalBefore := goal1 ,
             goalAfter := "",
             tactic := "exact Or.inl h",
             usedConstants := #["Or.inl"],
           },
         ]
       }],
    }: Protocol.FrontendProcessResult),
  ]
 example : 1 + 2 = 3 := rfl
 example (p: Prop): p → p := by simp
 def test_frontend_process_sorry : Test :=
  let solved := "example : 1 + 2 = 3 := rfl\n"
  let withSorry := "example (p: Prop): p → p := sorry"
  [
    let file := s!"{solved}{withSorry}"
    let goal1: Protocol.Goal := {
      name := "_uniq.6",
      target := { pp? := .some "p → p" },
      vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
    }
    step "frontend.process"
      [
        ("file", .str file),
        ("invocations", .bool false),
        ("sorrys", .bool true),
      ]
     ({
       units := [{
         boundary := (0, solved.utf8ByteSize),
       }, {
         boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
         goalStateId? := .some 0,
         goals := #[goal1],
         messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
       }],
    }: Protocol.FrontendProcessResult),
  ]
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
  -- Setup the environment for execution
  let context: Context := {
@ -249,8 +182,6 @@ def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
    ("Manual Mode", test_automatic_mode false),
    ("Automatic Mode", test_automatic_mode true),
    ("env.add env.inspect", test_env_add_inspect),
    ("frontend.process invocation", test_frontend_process),
    ("frontend.process sorry", test_frontend_process_sorry),
  ]
  tests.map (fun (name, test) => (name, runTest env test))
--- a/Test/Main.lean
+++ b/Test/Main.lean
@ -1,11 +1,10 @@
 import LSpec
 import Test.Environment
 import Test.Frontend
 import Test.Integration
 import Test.Library
 import Test.Metavar
 import Test.Proofs
-import Test.Delate
+import Test.Serial
 import Test.Tactic
 -- Test running infrastructure
@ -45,12 +44,11 @@ def main (args: List String) := do
  let suites: List (String × List (String × IO LSpec.TestSeq)) := [
    ("Environment", Environment.suite),
    ("Frontend", Frontend.suite env_default),
    ("Integration", Integration.suite env_default),
    ("Library", Library.suite env_default),
    ("Metavar", Metavar.suite env_default),
    ("Proofs", Proofs.suite env_default),
-    ("Delate", Delate.suite env_default),
+    ("Serial", Serial.suite env_default),
    ("Tactic/Congruence", Tactic.Congruence.suite env_default),
    ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
    ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -1,6 +1,6 @@
 import LSpec
 import Pantograph.Goal
-import Pantograph.Delate
+import Pantograph.Serial
 import Test.Common
 import Lean
@ -66,7 +66,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
  let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultElabContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
  let coreM := metaM.run'
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -3,7 +3,7 @@ Tests pertaining to goals with no interdependencies
 -/
 import LSpec
 import Pantograph.Goal
-import Pantograph.Delate
+import Pantograph.Serial
 import Test.Common
 namespace Pantograph.Test.Proofs
@ -74,7 +74,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
  let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultElabContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
  let coreM := metaM.run'
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -1,10 +1,10 @@
 import LSpec
-import Pantograph.Delate
+import Pantograph.Serial
 import Test.Common
 import Lean
 open Lean
-namespace Pantograph.Test.Delate
+namespace Pantograph.Test.Serial
 open Pantograph
@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
        | .ok expr => pure expr
        | .error e => return elabFailure e
      return LSpec.check source ((← serializeExpressionSexp expr) = target)
-    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultElabContext)
+    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
    return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
    LSpec.TestSeq.done
@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
    let testCaseName := target.take 10
    let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext)
+  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
 -- Instance parsing
 def test_instance (env: Environment): IO LSpec.TestSeq :=
@ -106,4 +106,4 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
    ("Instance", test_instance env),
  ]
-end Pantograph.Test.Delate
+end Pantograph.Test.Serial
--- a/flake.lock
+++ b/flake.lock
@ -5,11 +5,11 @@
        "nixpkgs-lib": "nixpkgs-lib"
      },
      "locked": {
-        "lastModified": 1730504689,
+        "lastModified": 1709336216,
-        "narHash": "sha256-hgmguH29K2fvs9szpq2r3pz2/8cJd2LPS+b4tfNFCwE=",
+        "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
        "owner": "hercules-ci",
        "repo": "flake-parts",
-        "rev": "506278e768c2a08bec68eb62932193e341f55c90",
+        "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
        "type": "github"
      },
      "original": {
@ -18,112 +18,208 @@
        "type": "github"
      }
    },
-    "flake-parts_2": {
+    "flake-utils": {
      "inputs": {
        "nixpkgs-lib": "nixpkgs-lib_2"
      },
      "locked": {
-        "lastModified": 1727826117,
+        "lastModified": 1656928814,
-        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
+        "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
-        "owner": "hercules-ci",
+        "owner": "numtide",
-        "repo": "flake-parts",
+        "repo": "flake-utils",
-        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
+        "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
        "type": "github"
      },
      "original": {
-        "owner": "hercules-ci",
+        "owner": "numtide",
-        "repo": "flake-parts",
+        "repo": "flake-utils",
        "type": "github"
      }
    },
-    "lean4-nix": {
+    "lean": {
      "inputs": {
-        "flake-parts": "flake-parts_2",
+        "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs"
+        "lean4-mode": "lean4-mode",
        "nix": "nix",
        "nixpkgs": "nixpkgs_2",
        "nixpkgs-old": "nixpkgs-old"
      },
      "locked": {
-        "lastModified": 1731711316,
+        "lastModified": 1719788866,
-        "narHash": "sha256-s5u+A2/Ea9gPveB5wwVM5dWW0NST6kamDsTeovGuLEs=",
+        "narHash": "sha256-kB2cp1XJKODXiuiKp7J5OK+PFP+sOSBE5gdVNOKWCPI=",
-        "owner": "lenianiva",
+        "owner": "leanprover",
-        "repo": "lean4-nix",
+        "repo": "lean4",
-        "rev": "136fc6057c48de970579e960b62421e9c295b67d",
+        "rev": "3b58e0649156610ce3aeed4f7b5c652340c668d4",
        "type": "github"
      },
      "original": {
-        "owner": "lenianiva",
+        "owner": "leanprover",
-        "repo": "lean4-nix",
+        "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,
+        "lastModified": 1722857503,
-        "narHash": "sha256-ZMqbvCqR/gHXRuIkuo7b0Yp9N1vOQR7xnrcy/SeIBoQ=",
+        "narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=",
-        "owner": "argumentcomputer",
+        "owner": "lurk-lab",
        "repo": "LSpec",
-        "rev": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
+        "rev": "8a51034d049c6a229d88dd62f490778a377eec06",
        "type": "github"
      },
      "original": {
-        "owner": "argumentcomputer",
+        "owner": "lurk-lab",
-        "ref": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
+        "ref": "8a51034d049c6a229d88dd62f490778a377eec06",
        "repo": "LSpec",
        "type": "github"
      }
    },
    "nix": {
      "inputs": {
        "lowdown-src": "lowdown-src",
        "nixpkgs": "nixpkgs",
        "nixpkgs-regression": "nixpkgs-regression"
      },
      "locked": {
        "lastModified": 1657097207,
        "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
        "owner": "NixOS",
        "repo": "nix",
        "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
        "type": "github"
      },
      "original": {
        "owner": "NixOS",
        "repo": "nix",
        "type": "github"
      }
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1728500571,
+        "lastModified": 1653988320,
-        "narHash": "sha256-dOymOQ3AfNI4Z337yEwHGohrVQb4yPODCW9MDUyAc4w=",
+        "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
-        "owner": "nixos",
+        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "d51c28603def282a24fa034bcb007e2bcb5b5dd0",
+        "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
        "type": "github"
      },
      "original": {
-        "owner": "nixos",
+        "owner": "NixOS",
-        "ref": "nixos-24.05",
+        "ref": "nixos-22.05-small",
        "repo": "nixpkgs",
        "type": "github"
      }
    },
    "nixpkgs-lib": {
      "locked": {
-        "lastModified": 1730504152,
+        "dir": "lib",
-        "narHash": "sha256-lXvH/vOfb4aGYyvFmZK/HlsNsr/0CVWlwYvo2rxJk3s=",
+        "lastModified": 1709237383,
-        "type": "tarball",
+        "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
-        "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
+        "owner": "NixOS",
        "repo": "nixpkgs",
        "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
        "type": "github"
      },
      "original": {
-        "type": "tarball",
+        "dir": "lib",
-        "url": "https://github.com/NixOS/nixpkgs/archive/cc2f28000298e1269cea6612cd06ec9979dd5d7f.tar.gz"
+        "owner": "NixOS",
        "ref": "nixos-unstable",
        "repo": "nixpkgs",
        "type": "github"
      }
    },
-    "nixpkgs-lib_2": {
+    "nixpkgs-old": {
      "flake": false,
      "locked": {
-        "lastModified": 1727825735,
+        "lastModified": 1581379743,
-        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
-        "type": "tarball",
+        "owner": "NixOS",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
+        "repo": "nixpkgs",
        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
        "type": "github"
      },
      "original": {
-        "type": "tarball",
+        "owner": "NixOS",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
+        "ref": "nixos-19.03",
        "repo": "nixpkgs",
        "type": "github"
      }
    },
    "nixpkgs-regression": {
      "locked": {
        "lastModified": 1643052045,
        "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
        "owner": "NixOS",
        "repo": "nixpkgs",
        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
        "type": "github"
      },
      "original": {
        "owner": "NixOS",
        "repo": "nixpkgs",
        "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
        "type": "github"
      }
    },
    "nixpkgs_2": {
      "locked": {
-        "lastModified": 1731386116,
+        "lastModified": 1686089707,
-        "narHash": "sha256-lKA770aUmjPHdTaJWnP3yQ9OI1TigenUqVC3wweqZuI=",
+        "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
        "owner": "NixOS",
        "repo": "nixpkgs",
        "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
        "type": "github"
      },
      "original": {
        "owner": "NixOS",
        "ref": "nixpkgs-unstable",
        "repo": "nixpkgs",
        "type": "github"
      }
    },
    "nixpkgs_3": {
      "locked": {
        "lastModified": 1711703276,
        "narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
        "owner": "nixos",
        "repo": "nixpkgs",
-        "rev": "689fed12a013f56d4c4d3f612489634267d86529",
+        "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
        "type": "github"
      },
      "original": {
        "owner": "nixos",
-        "ref": "nixos-24.05",
+        "ref": "nixos-unstable",
        "repo": "nixpkgs",
        "type": "github"
      }
@ -131,9 +227,9 @@
    "root": {
      "inputs": {
        "flake-parts": "flake-parts",
-        "lean4-nix": "lean4-nix",
+        "lean": "lean",
        "lspec": "lspec",
-        "nixpkgs": "nixpkgs_2"
+        "nixpkgs": "nixpkgs_3"
      }
    }
  },
--- a/flake.nix
+++ b/flake.nix
@ -2,11 +2,14 @@
  description = "Pantograph";
  inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-24.05";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
    flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix.url = "github:lenianiva/lean4-nix";
+    lean = {
      # Do not follow input's nixpkgs since it could cause build failures
      url = "github:leanprover/lean4?ref=v4.10.0-rc1";
    };
    lspec = {
-      url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
+      url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
      flake = false;
    };
  };
@ -15,7 +18,7 @@
    self,
    nixpkgs,
    flake-parts,
-    lean4-nix,
+    lean,
    lspec,
    ...
  } : flake-parts.lib.mkFlake { inherit inputs; } {
@ -26,16 +29,13 @@
      "x86_64-darwin"
    ];
    perSystem = { system, pkgs, ... }: let
-      pkgs = import nixpkgs {
+      leanPkgs = lean.packages.${system};
-        inherit system;
+      lspecLib = leanPkgs.buildLeanPackage {
        overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ];
      };
      lspecLib = pkgs.lean.buildLeanPackage {
        name = "LSpec";
        roots = [ "Main" "LSpec" ];
        src = "${lspec}";
      };
-      project = pkgs.lean.buildLeanPackage {
+      project = leanPkgs.buildLeanPackage {
        name = "Pantograph";
        roots = [ "Pantograph" ];
        src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
@ -46,7 +46,7 @@
            !(pkgs.lib.hasSuffix "Repl.lean" path);
        });
      };
-      repl = pkgs.lean.buildLeanPackage {
+      repl = leanPkgs.buildLeanPackage {
        name = "Repl";
        roots = [ "Main" "Repl" ];
        deps = [ project ];
@ -57,7 +57,7 @@
            !(pkgs.lib.hasSuffix ".md" path);
        });
      };
-      test = pkgs.lean.buildLeanPackage {
+      test = leanPkgs.buildLeanPackage {
        name = "Test";
        # NOTE: The src directory must be ./. since that is where the import
        # root begins (e.g. `import Test.Environment` and not `import
@ -72,25 +72,24 @@
      };
    in rec {
      packages = {
-        inherit (pkgs.lean) lean lean-all;
+        inherit (leanPkgs) lean lean-all;
-        inherit (project) sharedLib iTree;
+        inherit (project) sharedLib;
        inherit (repl) executable;
        default = repl.executable;
      };
      legacyPackages = {
-        inherit project;
+        inherit project leanPkgs;
        leanPkgs = pkgs.lean;
      };
      checks = {
        test = pkgs.runCommand "test" {
-          buildInputs = [ test.executable pkgs.lean.lean-all ];
+          buildInputs = [ test.executable leanPkgs.lean-all ];
        } ''
          #export LEAN_SRC_PATH="${./.}"
          ${test.executable}/bin/test > $out
        '';
      };
      devShells.default = pkgs.mkShell {
-        buildInputs = [ pkgs.lean.lean-all pkgs.lean.lean ];
+        buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
      };
    };
  };
--- a/lake-manifest.json
+++ b/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": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
   "rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
   "name": "LSpec",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
+   "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "pantograph",
--- a/lakefile.lean
+++ b/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]
--- a/2
+++ b/2
@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.10.0-rc1
`@ -1 +1 @@`
	`leanprover/lean4:v4.12.0`	`leanprover/lean4:v4.10.0-rc1`