| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #12496
|
|
We provide the closure of the dependencies manually.
This is still a hack, but not so bad given that the `source`'d files
still do contain that duplication too.
Dune should provide this functionality so we can replace both this
rule and the source files. Actually, that's not hard to implement,
`utop` already supports a printer attribute so these are loaded
automatically, so the ocamldebug mode could do the same.
Should fix #11716
|
|
We also workaround problem #11405 , however, this should be reverted
once the problem is fixed in OCaml upstream.
|
|
Works fine here, cc: #9975
|
|
- use coqc instead of coqtop (since -compile doesn't work anymore this
is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users
The dune-dbg dependencies are still broken ;_;
|
|
|
|
This fixes a problem reported by @Zimmi48 in #8948, IMHO we should be
able to have a clean build of core Coq.
|
|
|
|
Now that the checker is using the regular kernel files it can also use
the normal printers.
|
|
As noted by Gäetan, we didn't compile these. We also provide a recipe
to run `ocamldebug`. Try (after a build):
```
dune exec dev/dune-dbg
(ocd) source dune_db
```
or
```
dune exec dev/dune-dbg checker
(ocd) source checker_dune_db
```
for the checker.
|
