Negative lean kernel tests

Stream: lean4

[Aaron Hill]

If someone is implementing an external type checker (using lean4export), are there any 'negative' tests available to use? It would be useful to have:

• Invalid lean4export files that should cause a correctly implemented checker to produce an error
• Lean4 files that manually call Lean.addDecl with invalid declarations that should fail to typecheck in the kernel

I saw a couple of uses of 'addDecl' in the lean4 tests that produce "error: (kernel)" - are there more of these that I can use to help with checker testing?

cc @Julian Berman

[Chris Bailey]

I have a few in the test suite for the rust checker here, the negative ones are labelled as should_panic in the runner here.

In some cases it can be difficult to make negative tests because it's not feasible to make the whole lean environment by hand, so you need the lean code comprising the test cases to be admissible in order to use the exporter. You can get around this to some extent by either exporting then making small modifications, or by using unsafe (maybe other metaprogramming would be usable here too).

Off the top of my head, some other ones:

• Declarations containing undeclared universe variables (e.g. asserting a type of Sort u but with an empty uparams array)
• Declarations containing free variables or loose bound variables
• Expr.const items with the wrong number of levels for the corresponding declaration
• Expr.const items that reference a nonexistent declaration
• Expr.proj items with an impermissibly high index, or a name that isn't a structure.
• Environments trying to reuse the same declaration name
• Inductives with nonpositive occurrences
• Constructors that quantify over an impermissibly large argument
• Constructors for a type A that purport to return an element of B

[Julian Berman]

We ran the nanoda ones -- I think we're still going to try to put together a few more because we noticed even if we completely nerfed all the declaration checking functions and made them do nothing, we still only had 2 of the tests fail -- so we want to be sure we've actually written something which is really doing stuff!

The examples you just gave should be super helpful! (as was the rest of what you put together clearly!)

[Chris Bailey]

Julian Berman said:

We ran the nanoda ones -- I think we're still going to try to put together a few more because we noticed even if we completely nerfed all the declaration checking functions and made them do nothing, we still only had 2 of the tests fail

If we're still talking about the nanoda ones, some of them are supposed to fail because of the way they interact with the axiom whitelist in the config file, which may or may not apply to what you're doing. IIRC the main branch of lean4export skips unsafe declarations, so if you're using any of the test source files that have unsafe items without using the forked lean4export you may be getting less out the back than expected.

Let me know if I can be of assistance or potentially save you some time. Is it public yet?

[Julian Berman]

Thanks!! We're not done yet with the actual type checker (possibly by at least a few more days work, which we're doing sporadically), but what we're working on is here: https://github.com/Julian/rpylean I suspect the next time we meet we'll probably try to collect some of these into a suite

[Julian Berman]

(What's there doesn't run the Nanoda suite quite yet even, I see Aaron today got one of the additional tests working, yay.)