coq/dev/db, branch master The formal proof system [build] Refactoring to config lib and ocamldebug tweaks. 2018-10-22T22:42:04+00:00 Emilio Jesus Gallego Arias 2018-10-17T13:24:15+00:00 1db19a8f454e0f8c5a60101c87ccd38e0883d530 We make `config` into a properly library. This is more uniform and useful for some clients. This also matches what was done in Dune. Next step would be to push dependencies on `Coq_config` upwards, only the actual toplevel binaries should depend on it. We also remove the stale `camlp5.dbg` and refactor the dbg files a bit, isolating the bits that are specific to the plugin / lib building method used by makefile. 
We make `config` into a properly library. This is more uniform and
useful for some clients. This also matches what was done in Dune.

Next step would be to push dependencies on `Coq_config` upwards, only
the actual toplevel binaries should depend on it.

We also remove the stale `camlp5.dbg` and refactor the dbg files a
bit, isolating the bits that are specific to the plugin / lib building
method used by makefile.
Add printers to dev/db 2017-12-22T15:41:33+00:00 Gaëtan Gilbert 2017-12-22T15:35:22+00:00 7b9f83224e13b21fcb5bd1b3742f52070c3299e4 






Reorder dev/db
2017-12-22T15:41:33+00:00

Gaëtan Gilbert

2017-12-22T15:31:20+00:00

897b37129850002953be4426ffc852da63c8f4e6












Cleanup debug printers a bit, add generated mli.
2017-12-22T15:36:32+00:00

Gaëtan Gilbert

2017-12-16T09:58:52+00:00

87cbd64254f33439882156d9a297a6a2f6886057












Adding a debugging printer for ident maps whose codomain type is unknown.
2017-11-08T17:04:13+00:00

Hugo Herbelin

2017-11-08T17:00:00+00:00

d7da4e1dfc58942ceb91fb24afe4751d6fb50cc9

Actually, ocaml is apparently doing well. If there is a printer for 'a
Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined
existing ones, so, it is apparently not a problem to have overlapping
printer.





Actually, ocaml is apparently doing well. If there is a printer for 'a
Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined
existing ones, so, it is apparently not a problem to have overlapping
printer.







Adding debug printers related to universes in the default debugger source file.
2017-07-14T12:10:30+00:00

Pierre-Marie Pédrot

2017-07-14T12:10:30+00:00

75bc9715c48f7b4f983d22cab27ce890d5d500a4












Introducing a new EConstr.t type to perform the nf_evar operation on demand.
2016-11-08T17:35:12+00:00

Pierre-Marie Pédrot

2016-09-01T15:52:44+00:00

a42795cc1c2a8ed3efa9960af920ff7b16d928f0












Merge branch 'v8.6'
2016-10-08T15:41:15+00:00

Pierre-Marie Pédrot

2016-10-08T15:41:15+00:00

1a9fe0dfe837ccbee25e9ecf19a7b2e7768a7958












Adding debugging printer for Genarg.ArgT.t.
2016-10-08T14:50:13+00:00

Hugo Herbelin

2016-09-13T10:43:52+00:00

8110e9cbd6d70960a221c316774460f6ad6dc5e9












No more dev/printers.cma
2016-07-26T14:32:49+00:00

Pierre Letouzey

2016-07-25T13:56:24+00:00

32be84c5ba384f93b350a551d7bbbeec03768046

 This file was only used during ocamldebug sessions (in the dev/db
 script). It was containing a large subset of the core cma files,
 up to the printing functions. There were a few notable exceptions,
 for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
 But printers.cma was troublesome to maintain : almost each time an ML file
 was added/removed/renamed in the core of Coq, dev/printers.mllib
 had to be edited, in addition to the directory-specific .mllib
 (kernel/kernel.mllib and co). So I propose here to kill this file,
 and put instead in dev/db several "load_printer" of the core cma files.

 For that to work, we need to compile kernel/kernel.cma with the right
 -dllib and -dllpath options, but that shouldn't hurt (on the contrary).
 We also source now the camlpX cma in dev/db, via a new generated file
 dev/camlp4.dbg containing a load_printer of either gramlib.cma or
 camp4lib.cma.

 If one doesn't want to perform the whole "source db" at the start
 of an ocamldebug session, then the former "load_printer printers.cma"
 could be replaced by:

  source core.dbg
  load_printer top_printers.cmo

 See for instance the minimal dev/base_db.





 This file was only used during ocamldebug sessions (in the dev/db
 script). It was containing a large subset of the core cma files,
 up to the printing functions. There were a few notable exceptions,
 for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug.
 But printers.cma was troublesome to maintain : almost each time an ML file
 was added/removed/renamed in the core of Coq, dev/printers.mllib
 had to be edited, in addition to the directory-specific .mllib
 (kernel/kernel.mllib and co). So I propose here to kill this file,
 and put instead in dev/db several "load_printer" of the core cma files.

 For that to work, we need to compile kernel/kernel.cma with the right
 -dllib and -dllpath options, but that shouldn't hurt (on the contrary).
 We also source now the camlpX cma in dev/db, via a new generated file
 dev/camlp4.dbg containing a load_printer of either gramlib.cma or
 camp4lib.cma.

 If one doesn't want to perform the whole "source db" at the start
 of an ocamldebug session, then the former "load_printer printers.cma"
 could be replaced by:

  source core.dbg
  load_printer top_printers.cmo

 See for instance the minimal dev/base_db.