I intend to create a new metamath org repository named "lamp-guide"

32 views
Skip to first unread message

David A. Wheeler

unread,
May 29, 2023, 6:26:36 PM5/29/23
to Metamath Mailing List
All:

I intend to create a new metamath org repository named "lamp-guide"
to host the "Metamath-lamp Guide".
This is at the request of the maintainer of metamath-lamp.
Below is the backstory.

Let me know ASAP if there's a problem. I can't imagine what the problem
would be, though, so I intend to do this soon.
Everything is under the MIT license, though if that's
an issue I think I can simply relicense it as the author of this material
(e.g., as MIT OR CC-BY-4.0).

--- David A. Wheeler

====

I've been working to create a guide for the
proof assistant metamath-lamp. The guide currently in the
metamath-lamp repo:
https://github.com/expln/metamath-lamp

However, the maintainer of metamath-lamp (Igor Ieskov / @expln)
would prefer that the guide be in its own separate repository instead
of being intermingled with the code:
https://github.com/expln/metamath-lamp/issues/65

I intend to keep the
history of the guide's development in case that's useful, so I'll
probably make a copy of it using git & push it back.
(I don't want GitHub to say "this is a fork of XYZ", so I probably
won't use GitHub's fork command unless someone knows how to undo that).

David A. Wheeler

unread,
May 29, 2023, 8:23:19 PM5/29/23
to Metamath Mailing List

> On May 29, 2023, at 6:26 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
> All:
>
> I intend to create a new metamath org repository named "lamp-guide"
> to host the "Metamath-lamp Guide".

I have created a new metamath repo:
<https://github.com/metamath/lamp-guide>

to host this guide. I believe this repo implements this:
https://github.com/expln/metamath-lamp/issues/65

Please file issues if you see any issues, or even better, please provide pull requests :-).

--- David A. Wheeler

Reply all
Reply to author
Forward
0 new messages