Mac Malone

This issue has been plaguing me for a while in VSCode and is very unfortunate, It kills all the nice interactive features that are major positives of Lean. However, I...

Fyi, I posted a thread on Zulip ([leanpkg++ idea](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/leanpkg.2B.2B.20idea.20.5BRFC.5D/near/239484267)) related to a design idea for the new `leanpkg`. The basic idea is for developers to write package configuration in Lean...

@saulshanabrook I agree that declarative specification of dependencies is useful. However, I think that can be accomplished even with an interpreted configuration through the use of a lock file. Also,...

@Kha > The abstract rule is that the structure of the parser output should uniquely determine the parser call graph/grammar derivation tree that produced it. By "structure" (of a Syntax...

> Because we want a quotation pattern in a semantic transformation, e.g. a macro, that used `fun` to still match if the user wrote `λ`. And avoid the code explosion...

> > Could not tokens with multiple different spelling just be parsed as a node with a unique kind rather than different atoms? > > I can't make sense of...

As an aside: > The real solution here is a strongly-typed syntax type indexed by the syntax kind. I think this would be a wonderful long term goal and wasn't...

@Kha, I appear to have hit a weird bug in the Linux (non-release) and Nix CI builds when linking the executables. It is for some reason looking in `libleanshared` for...

@Kha > I think the main issue was that outParams do not play well with coercions. I don't know if it works for you because you still have the `[Quote...

@Kha > You can try purging the ccache cache as in [Kha@524ae5a](https://github.com/Kha/lean4/commit/524ae5abf72e25287b753382b267519e4e43870d). If it's really that, it's starting to get annoying...' Good new, ccache is not at fault! Bad news,...