Incorrectly adding propext with nanoda kernel

For theorems that don't use propext (see below for a minimum example), they pass the check with the Lean default kernel...

Exporting #[mwe, Quot.sound, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList] from Solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!

...but not the nanoda kernel.

Running nanoda kernel on solution
Error: export file declares unpermitted axiom "propext"

run with `-h` or `--help` for help
uncaught exception: resource vanished (error code: 32, broken pipe)

This is because Nat.xor depends on propext and is unconditionally exported as part of primitiveTargets.

https://github.com/leanprover/comparator/blob/3afea238d63125383110f8b59acaf11d7788c3e1/Main.lean#L222

That's why it shows up in the export list despite not being used in the example. If I'm reading the code right, for the default kernel axioms are only checked for theorems and definitions in the solution, and not the more general exportTargets list that includes primitiveTargets. However, since nanoda is ran on the entire exportTargets which includes Nat.xor, it detects the use of propext and gives the error.

https://github.com/leanprover/comparator/blob/3afea238d63125383110f8b59acaf11d7788c3e1/Main.lean#L252

https://github.com/leanprover/comparator/blob/3afea238d63125383110f8b59acaf11d7788c3e1/Main.lean#L258-L259

https://github.com/leanprover/comparator/blob/3afea238d63125383110f8b59acaf11d7788c3e1/Main.lean#L267

https://github.com/leanprover/comparator/blob/3afea238d63125383110f8b59acaf11d7788c3e1/Main.lean#L254

Note that directly running nanoda on the theorem mwe with

lake env lean4export Solution -- mwe | nanoda_bin nanoda_config.json

using the nanoda configuration from comparator

{"nat_extension":true,"permitted_axioms":[],"string_extension":true,"unpermitted_axiom_hard_error":true,"use_stdin":true}

https://github.com/leanprover/comparator/blob/3afea238d63125383110f8b59acaf11d7788c3e1/Main.lean#L158-L164

passes the check as expected.

Challenge.lean

theorem mwe (n : Nat) : n = n := sorry

Solution.lean

theorem mwe (n : Nat) : n = n := rfl

config.json

{
    "challenge_module": "Challenge",
    "solution_module": "Solution",
    "theorem_names": ["mwe"],
    "permitted_axioms": [],
    "enable_nanoda": true
}

lakefile.toml

name = "comparatortest"
version = "0.1.0"

[[lean_lib]]
name = "Solution"

[[lean_lib]]
name = "Challenge"

Start in Main.lean around the primitiveTargets and exportTargets definitions at the linked lines, then inspect the default-kernel and nanoda checks. Reproduce the issue with the provided Challenge.lean, Solution.lean, config.json, and lakefile.toml, including the direct nanoda command. Done means a theorem that does not use propext passes both checks without the unconditional Nat.xor export causing an error.