Kani compilation fails when running cargo kani in a proc macro crate with `crate-type` specified.

[celinval]

I tried this code:

// src/lib.rs
#[kani::proof]
fn noop() {}

# Cargo.toml
[package]
name = "proc_macro_lib"
version = "0.1.0"
edition = "2021"

[lib]
name = "lib"
crate-type = ["lib"]
proc-macro = true
path = "src/lib.rs"

using the following command line invocation:

cargo kani

with Kani version: 0.17.0

I expected to see this happen: Verification succeed or Kani fail with a reasonable error

Instead, this happened: Kani compilation fail:

   Compiling proc_macro_lib v0.1.0 (/tmp/lib-pmacro)
error: Unrecognized option: 'reachability'

error: could not compile `proc_macro_lib`
Error: cargo exited with status exit status: 101

[celinval]

We currently don't support proc-macro verification, but the mechanism that we use to detect proc-macros doesn't work here. I created an issue to see if cargo metadata can include more information that will allow us to detect an issue like that:

rust-lang/cargo#11508