Extract Constants [ ... ] fails if list contains unused constants

[intoverflow]

(I am working from the prims branch; apologies if this has been fixed in a later commit.)

The issue is best illustrated by an example:

From CertiCoq.Plugin Require Import CertiCoq.

Axiom my_fast_add: nat -> nat.

Definition foo: nat := 0.

(* This works: *)
CertiCoq Compile
    foo
    Extract Constants [
    ]
    Include [
    ].

Definition bar: nat := my_fast_add foo.

(* This also works: *)
CertiCoq Compile
    bar
    Extract Constants [
        my_fast_add => "my_primitive_fast_add"
    ]
    Include [
    ].

(* This does not work: *)
CertiCoq Compile
    foo
    Extract Constants [
        my_fast_add => "my_primitive_fast_add"
    ]
    Include [
    ].
(* Error message:
Could not compile: Constant example.my_fast_add not found in environment
*)

The error is raised by find_prim_arrity during register_prims in theories/Compiler/pipeline.v.

I suspect the environment for the extraction target does not include unused axioms/definitions.

The fix: if a constant is not used, it is safe to give it any arity we want (is this right? I'm only guessing here). The attached patch exploits this by modifying find_prim_arrity to return 0 for primitives that cannot be found in the environment.

tcarstens@pop-os:~/formal_methods/certicoq$ git diff
diff --git a/theories/Compiler/pipeline.v b/theories/Compiler/pipeline.v
index 85d7990d..ad4ee543 100644
--- a/theories/Compiler/pipeline.v
+++ b/theories/Compiler/pipeline.v
@@ -40,9 +40,10 @@ Definition find_global_decl_arrity (gd : Ast.global_decl) : error nat :=
 
 Fixpoint find_prim_arrity (env : Ast.global_env) (pr : kername) : error nat :=
   match env with
-  | [] => Err ("Constant " ++ string_of_kername pr ++ " not found in environment")
+  (* | [] => Err ("Constant " ++ string_of_kername pr ++ " not found in environment") *)
+  | [] => Ret 0
   | (n, gd) :: env =>
-    if eq_kername pr n then find_global_decl_arrity  gd
+    if eq_kername pr n then find_global_decl_arrity gd
     else find_prim_arrity env pr
   end.

tcarstens@pop-os:~/formal_methods/certicoq$ 

[intoverflow]

Quick update: I discussed this issue with @zoep , @andrew-appel , and @john-ml earlier this week. We concluded the following:

1. We want Extract Constants [] to be able to detect typos and report them to the user. The workaround given above cannot do that; therefore we should not adopt it.
2. The issue appears to be that MetaCoq's context only includes definitions that appear as free variables in the Compile target.
3. Ideally: find_prim_arrity should check to see if pr is defined; if not, then pr is probably a typo and an error should be reported.

I'll ask around to see if there's an easy way to do this; if not I'll reach out to MetaCoq (cc @joom - please ping me if you happen to have any tips)

[joom]

This problem doesn't occur anymore.