dk meta -m meta.dk requires meta.dko

[aarneranta]

It can be that I just don't know how to use 'dk meta' properly, and in that case I would be grateful for a pointer to a working example and documentation. But still, uncaught exceptions are always good to fix.

A minimal example:

• file nopi.dk [x] enc.El _ x --> Elem x. [a, b]enc.Pi _ _ _ a (x => b) --> (x : a) -> b.

• file initlean.dk Nat_succ : enc.El (lvl.s lvl.z) (enc.Pi (lvl.s lvl.z) (lvl.s lvl.z) (lvl.imax (lvl.s lvl.z) (lvl.s lvl.z)) Nat (x0 : enc.El (lvl.s lvl.z) Nat => Nat)) .

Command: dk meta -m nopi.dk initlean.dk

Output: dkcheck: internal error, uncaught exception: Api.Files.Files_error(_)

I have tried a few things without success

• just one of the two rules
• qualifying and unqualifying constants in the nopi.dk file

What works, however, is an empty nopi.dk file. The result is then initlean.dk pretty-printed. Hence I guess there is something wrong in the way I write the nopu.dk file.

[francoisthire]

I did not use dkmeta for a while now, so I am a bit rusty and I wish the error message could be clearer. The fact the error was raised by the Api.Files module let me think there is an error related to where dkmeta expects to find some files.

Things to check:

• It might be possible you need to run dk check first for initlean.dk which generates a dko file. This dko file may be used by dk meta.

If it does not work, on the short term, I would recommend to add debug logging to understand the issue, or maybe run with OCAMLRUNPARAM=b (or something similar) to get a backtrace. This could help to understand the issue.

[aarneranta]

Hi François,

Thanks for the quick reply!

One problem is that the file I am trying to convert is a large generated file that does not pass dk check. I can try to fix this later. But as far as I understand, rewrite should not require well-typedness. Is there a way to build a .dko in that case?

Regards

Aarne

---

From: FrançoisT @.> Sent: 16 April 2025 15:17 To: Deducteam/Dedukti @.> Cc: Aarne Ranta @.>; Author @.> Subject: Re: [Deducteam/Dedukti] internal error with 'dk meta': Api.Files.Files_error(_) (Issue #335)

I did not use dkmeta for a while now, so I am a bit rusty and I wish the error message could be clearer. The fact the error was raised by the Api.Files module let me think there is an error related to where dkmeta expects to find some files.

Things to check:

• It might be possible you need to run dk check first for initlean.dk which generates a dko file. This dko file may be used by dk meta.

If it does not work, on the short term, I would recommend to add debug logging to understand the issue, or maybe run with OCAMLRUNPARAM=b (or something similar) to get a backtrace. This could help to understand the issue.

— Reply to this email directly, view it on GitHubhttps://github.com/Deducteam/Dedukti/issues/335#issuecomment-2809562150, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAWBQXN6NWNWDJW4ACS4ETL2ZZJ53AVCNFSM6AAAAAB3H275WCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDQMBZGU3DEMJVGA. You are receiving this because you authored the thread.Message ID: @.***>

[https://avatars.githubusercontent.com/u/2529963?s=20&v=4]francoisthire left a comment (Deducteam/Dedukti#335)https://github.com/Deducteam/Dedukti/issues/335#issuecomment-2809562150

I did not use dkmeta for a while now, so I am a bit rusty and I wish the error message could be clearer. The fact the error was raised by the Api.Files module let me think there is an error related to where dkmeta expects to find some files.

Things to check:

• It might be possible you need to run dk check first for initlean.dk which generates a dko file. This dko file may be used by dk meta.

If it does not work, on the short term, I would recommend to add debug logging to understand the issue, or maybe run with OCAMLRUNPARAM=b (or something similar) to get a backtrace. This could help to understand the issue.

— Reply to this email directly, view it on GitHubhttps://github.com/Deducteam/Dedukti/issues/335#issuecomment-2809562150, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAWBQXN6NWNWDJW4ACS4ETL2ZZJ53AVCNFSM6AAAAAB3H275WCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDQMBZGU3DEMJVGA. You are receiving this because you authored the thread.Message ID: @.***>

[francoisthire]

So I tried locally to reproduce your setup. I think, something useful would be to do a PR to add debugging information, for example:

diff --git a/api/files.ml b/api/files.ml
index 259e9b57..892d8cfd 100644
--- a/api/files.ml
+++ b/api/files.ml
@@ -105,7 +105,9 @@ exception File_error of file_error
 let fail_file_error ~red:_ exn =
   match exn with File_error err -> Some (string_of_error err) | _ -> None
 
-let _ = Errors.register_exception fail_file_error
+let _ = 
+  Printexc.register_printer (fun exn -> fail_file_error ~red:Fun.id exn |> Option.map (fun (_,_,exn) -> exn));
+  Errors.register_exception fail_file_error
 
 let get_file_exn load_path loc md =
   match file_status load_path md with

This will generate something like:

./dk.native  meta -I /tmp -m /tmp/meta.dk /tmp/test.dk 
dkcheck: internal error, uncaught exception:
         No object file (.dko) found for module meta located at /tmp/meta.dko

So indeed I was rusty. What is needed is to check the meta file, not the file to be rewritten. So you must generate a dko for the meta file at the moment.

In theory, it should not be necessary, it is a limitation of the current implementation (due to how rewrite rules are compiled).

To check this file, you might need to produce dko for the dependencies files too.

[fblanqui]

Does that mean that meta rules must preserve typing?