Use findlib instead of Boot.Env.native_cmi (#28)

Adapt to rocq-prover/rocq#20376

Author: SkySkimmer

.github/workflows/docker-action.yml

@@ -14,15 +14,15 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        image:
-          - 'coqorg/coq:dev'
+        coq_version:
+        - 'dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-ltac2-compiler.opam'
-          custom_image: ${{ matrix.image }}
+          coq_version: ${{ matrix.coq_version }}
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

src/tac2compile.ml

@@ -1110,11 +1110,9 @@ let error_compiler_failed e =
   CErrors.user_err msg
 
 let include_dirs () =
-  (* TODO make this work in -boot / dev shim mode *)
-  let open Boot.Env in
-  let env = init () in
+  let rocq = Findlib.package_directory "rocq-runtime" in
   (* engine for Proofview, kernel for Names *)
-  let core = List.map (fun x -> Path.to_string (native_cmi env x))
+  let core = List.map (fun x -> Filename.concat rocq x)
       [ "kernel"; "engine"; "plugins/ltac2" ]
   in
   let self = Findlib.package_directory "coq-ltac2-compiler" in