Skip to content

The issues from the latest dependency tracking

YAQING JIANG edited this page Aug 9, 2019 · 1 revision

I tried to use the latest version (commit 0cc4f19dd34f52ef4f354f861206dad361640458). With only core library (hol.ml) perhaps I should use a pin version (two commits before). I used the all json with ~json_proofs:false .

Here's what I found. Things might change (I did something wrong):

  1. "tracked_ids" in "theorem_idents" is always empty. (even if I don't set ~json_proofs:false )
  2. Theorems missing in both "identifier" table and "dependency" table. There's no way to recover the information.
Clone this wiki locally