Objective Caml - Среда, 9 мая 2012

Objective Caml

ocaml@conference.jabber.ru

Среда, 9 мая 2012< ^ >

Конфигурация комнаты

Участники комнаты

GMT+4
[01:04:19] Sun][ вышел(а) из комнаты
[01:43:31] Kakadu вышел(а) из комнаты
[02:16:38] Typhon вышел(а) из комнаты
[02:40:28] f[x] вышел(а) из комнаты: Computer went to sleep
[03:37:15] letrec вошёл(а) в комнату
[04:02:47] ftrvxmtrx вышел(а) из комнаты
[04:03:00] ftrvxmtrx вошёл(а) в комнату
[04:43:39] letrec вышел(а) из комнаты
[06:36:35] ftrvxmtrx вышел(а) из комнаты
[06:36:44] ftrvxmtrx вошёл(а) в комнату
[08:44:17] <gds> f[x]: да вот проблемка есть, для экстракции требует модули, используемые в .v:
$ coqc my.v
File "./my.v", line 1, characters 0-23:
Error: Cannot find library Listmap in loadpath
причём Listmap -- мой же модуль Listmap.v
И ещё что удивительно:
$ coqdep my.v
*** Warning: in file my.v, library Listmap.v is required and has not been found in loadpath!
*** Warning: in file my.v, library Types.v is required and has not been found in loadpath!
my.vo my.glob: my.v
вообще непонятно, даже coqdep *.v выдаёт подобную же хрень и генерит такие же ненужные тривиальные строчки вида "my.vo my.glob: my.v" для каждого модуля.  Вот тут хороший повод помучить #coq.
[09:37:14] <gds> мать его, достаточно " -I . " передавать.
В общем, вырисовывается такая логика: правило из "%.v" в ["%.vo"; "%.ml"], в этом правиле читаем вывод команды "coqdep -I . %.v" (кстати, как?  Unix недоступен для myocamlbuild.ml, т.е. только Sys.command во временный файл?), далее через аргумент "builder" пытаемся строить все .vo-файлы, требуемые для экстракции данного %.v (достаточно List.iter Outcome.ignore_good (builder [["a.vo"]; ["b.vo"]; ...])), затем уже запускаем собственно "coqc %.v", получая .vo и .ml.
f[x], по идее, схема звучит более-менее здраво?  (я не про специфику coq, а про специфику ocamlbuild.)  Sys.command и временный файл таки?
[09:52:49] ermine вошёл(а) в комнату
[10:23:09] ftrvxmtrx вышел(а) из комнаты
[11:22:14] Kakadu вошёл(а) в комнату
[11:29:48] ftrvxmtrx вошёл(а) в комнату
[12:06:20] Typhon вошёл(а) в комнату
[12:43:08] Sun][ вошёл(а) в комнату
[14:28:57] Sun][ вышел(а) из комнаты
[14:29:52] Typhon вышел(а) из комнаты
[15:27:44] letrec вошёл(а) в комнату
[16:41:59] ftrvxmtrx вышел(а) из комнаты
[16:42:13] ftrvxmtrx вошёл(а) в комнату
[18:35:48] Sun][ вошёл(а) в комнату
[19:07:50] f[x] вошёл(а) в комнату
[19:24:06] ftrvxmtrx вышел(а) из комнаты
[19:45:54] letrec вышел(а) из комнаты
[19:47:09] arhibot вошёл(а) в комнату
[19:48:45] arhibot вышел(а) из комнаты
[20:10:18] tilarids вошёл(а) в комнату
[20:11:46] ftrvxmtrx вошёл(а) в комнату
[21:10:25] <f[x]> gds: да, похоже на правду
[21:10:48] <f[x]> насчёт sys.command - там должно экспортироваться что-то похожее
[21:11:04] <f[x]> my_unix.run_and_read или как-то так
[21:11:17] <f[x]> посмотри в ocamlfind плагине
[21:12:38] <gds> f[x]: во, похоже -- значит туда и буду смотреть.  Впрочем, подумаю сделать через одно место: явно генерить .coqdep-файлы с результатом вывода "coqdep ... > ..." и их уже 1. требовать для .v -> .{ml,vo}, 2. разбирать с диска.  Или вообще нет смысла в таком?
[22:05:12] Typhon вошёл(а) в комнату
[22:05:33] ltt вошёл(а) в комнату
[22:07:24] ltt вышел(а) из комнаты
[22:07:57] ltt вошёл(а) в комнату
[22:12:32] Typhon вышел(а) из комнаты
[22:24:54] ltt вышел(а) из комнаты
[22:51:14] Kakadu вышел(а) из комнаты
[22:51:30] tilarids вышел(а) из комнаты: Computer went to sleep
[23:07:58] Sun][ вышел(а) из комнаты