Minimal `Logs` integration #1206

Halbaroth · 2024-08-12T14:58:26Z

This PR adds:

Logs as a new dependency;
Logs' sources for each debug flag;
A reporter that prints on the appropriate output (regular or
diagnostic) according to the source.

As explained in #785, we cannot do really better without breaking the API of Printer

This PR is rebased on #1204

See #1207 for an example using sources introduced here.

Notice that I create two sources for theories with a Shostak and Relation modules. An alternative implementation consists in prefixing all the messages in *_rel.ml by [Rel] as it does in the legacy code. I have no strong opinion on this choice.

I did not create a bijection between debug flags and sources because it is more flexible to use two different lists.
For instance, it could be useful to create flags that set different sources (and actually, --dd adt for instance set adt and adt_rel sources).

bclement-ocp · 2024-08-19T07:22:43Z

src/bin/js/worker_interface.ml

@@ -185,7 +185,7 @@ type options = {
  debug_cc : bool option;
  debug_combine : bool option;
  debug_constr : bool option;
-  debug_explanations : bool option;
+  debug_explanation : bool option;


The correct name for this feature is the plural "explanations"; please revert this change.

Please justify correct. The name of module is explanation. I did this modification because the current name of the debug flag is explanation too.

the current name of the debug flag is explanation too

I'd argue that this is incorrect as well (although I never noticed since I always write -d ex) ;)

What I mean is — there are multiple explanations used by Alt-Ergo that we want to debug; similar to debug_commands, debug_warnings, debug_triggers, debug_types, debug_intervals, etc. On the other hand the singular flags such as debug_bitv, debug_interpretation, debug_matching, debug_uf, etc. refer to a single data-structure / theory / step to debug (ignoring the fact that we duplicate the environment for case-split purposes).

"The correct name" was a bit strong, and I apologize — I don't think it matters too much either way. However I do believe that if it does not matter, it is best to not change whatever is there. Now that the change has been made let's keep it.

I don't think it's matter too. When I see a discrepancy in our naming conventions and I am modifying this part of the code, I try to reduce it a bit. I agree to rename explanation to explanations everywhere (but for the module name of course).

In fact, I removed the source from Explanation because --d explanations has no relation with this module. It increases the verbosity of explanations. We may add flags like --verbosity explanations, ....

bclement-ocp · 2024-08-19T07:27:43Z

src/bin/common/parse_command.ml

  let mk ~verbosity flags =
+    let module S = Sources in


I am not a big fan of using a global Sources module with all sources stuffed in. Since we are setting up sources in the Parse_command module which has everything has a dependency, would it be possible to have each module expose its own val src : Logs.src instead (like in the Logs examples in the documentation)?

Sure, this was my first design in fact...

Just, notice that some of them do not correspond with a module.

I'd say that the few that do not correspond with a module can either be:

Stuffed into options.ml for now, or

Moved to a relevant module (e.g. we could have fm_src in intervalCalculus.ml), or

Removed entirely as they are not used (we will figure out what to do with them at a later time)

bclement-ocp · 2024-08-20T15:59:09Z

src/bin/common/parse_command.ml

+    | Explanation (* deprecated *)
+    | Explanations


We can simply use "explanations". Cmdliner uses prefix completion so that -d explanation will still work the same (on the other hand having both "explanation" and "explanations" breaks -d ex).

Oh I do not know we can do that :) thanks

bclement-ocp · 2024-08-20T16:00:44Z

src/lib/reasoners/relation.ml

@@ -41,6 +41,9 @@ module Rel5 : Sig_rel.RELATION = Adt_rel

 module Rel6 : Sig_rel.RELATION = Ite_rel

+(* This source is unused. *)
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)


Maybe we don't need it then? I think all the other sources are also unused, why single this one out?

It is an artefact. I added it because I tried to add the source in the signature of Sig_rel, which was not a good idea. We do not want to build all the modules in Parse_commands just to setup up sources.

In fact, it was not an artefact. I can remove src from Sig_rel but I have to introduce an extra signature in all the modules *_rel.mli.

This PR adds: - `Logs` as a new dependency; - Logs' sources for each debug flag; - A reporter that prints on the appropriate output (regular or diagnostic) according to the source.

CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)

Halbaroth added the frontend label Aug 12, 2024

Halbaroth force-pushed the use-logs branch from 8265861 to 5e9fb2f Compare August 12, 2024 17:01

Halbaroth mentioned this pull request Aug 12, 2024

Use logs in Adt_rel #1207

Merged

bclement-ocp mentioned this pull request Aug 19, 2024

Logs #1068

Closed

bclement-ocp reviewed Aug 19, 2024

View reviewed changes

Halbaroth force-pushed the use-logs branch 5 times, most recently from 6134114 to 4bc1db8 Compare August 20, 2024 15:32

Halbaroth requested a review from bclement-ocp August 20, 2024 15:48

Halbaroth force-pushed the use-logs branch from 4bc1db8 to 3175fdd Compare August 20, 2024 15:49

bclement-ocp reviewed Aug 20, 2024

View reviewed changes

Halbaroth force-pushed the use-logs branch from 14fba13 to 9a61fae Compare August 21, 2024 14:02

Halbaroth added 3 commits August 21, 2024 16:03

Add minimal Logs integration

ca58a47

This PR adds: - `Logs` as a new dependency; - Logs' sources for each debug flag; - A reporter that prints on the appropriate output (regular or diagnostic) according to the source.

review changes

53adca8

review changes 2

9a61fae

Halbaroth requested a review from bclement-ocp August 22, 2024 11:03

bclement-ocp approved these changes Aug 22, 2024

View reviewed changes

Halbaroth merged commit dfcc900 into OCamlPro:next Aug 22, 2024
17 checks passed

bclement-ocp mentioned this pull request Sep 24, 2024

[new release] alt-ergo (4 packages) (2.6.0) ocaml/opam-repository#26609

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Minimal `Logs` integration #1206

Minimal `Logs` integration #1206

Halbaroth commented Aug 12, 2024 •

edited

Loading

bclement-ocp Aug 19, 2024

Halbaroth Aug 20, 2024 •

edited

Loading

bclement-ocp Aug 20, 2024

Halbaroth Aug 20, 2024

Halbaroth Aug 20, 2024 •

edited

Loading

bclement-ocp Aug 19, 2024

Halbaroth Aug 20, 2024

Halbaroth Aug 20, 2024 •

edited

Loading

bclement-ocp Aug 20, 2024

bclement-ocp Aug 20, 2024

Halbaroth Aug 20, 2024

bclement-ocp Aug 20, 2024

Halbaroth Aug 20, 2024 •

edited

Loading

Halbaroth Aug 20, 2024

Minimal Logs integration #1206

Minimal Logs integration #1206

Conversation

Halbaroth commented Aug 12, 2024 • edited Loading

Choose a reason for hiding this comment

Halbaroth Aug 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Aug 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Aug 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth Aug 20, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Minimal `Logs` integration #1206

Minimal `Logs` integration #1206

Halbaroth commented Aug 12, 2024 •

edited

Loading

Halbaroth Aug 20, 2024 •

edited

Loading

Halbaroth Aug 20, 2024 •

edited

Loading

Halbaroth Aug 20, 2024 •

edited

Loading

Halbaroth Aug 20, 2024 •

edited

Loading