Stream: Coq devs & plugin devs

Topic: Extraction and counting


view this post on Zulip Jason Gross (Oct 16 2022 at 06:46):

Does Extraction know how to count past 9? Or does anyone have a better hypothesis for generating code that errors with

File "src/ExtractionOCaml/with_bedrock2_saturated_solinas.ml", line 648565, characters 12-25:
648565 |           { package_name0 =
                     ^^^^^^^^^^^^^
Error: Unbound module Coq__10
Hint: Did you mean Coq__1?

(The bad highlighting is due to https://github.com/ocaml/ocaml/issues/11629)

view this post on Zulip Jason Gross (Oct 16 2022 at 08:00):

Reported at https://github.com/coq/coq/issues/16677

view this post on Zulip Jason Gross (Oct 16 2022 at 08:01):

This generated code looks very suspicious

{
  package_name0 = opts.parsed_synthesize_options.internal_package_name;
  class_name0 = opts.parsed_synthesize_options.internal_class_name;
  inline0 = opts.parsed_synthesize_options.inline;
  Coq__11.inline_internal = opts.parsed_synthesize_options.inline_internal;
  no_select0 = opts.parsed_synthesize_options.no_select;
  Coq__12.use_mul_for_cmovznz = opts.parsed_synthesize_options.use_mul_for_cmovznz;
  Coq__13.emit_primitives = opts.parsed_synthesize_options.emit_primitives;
  should_split_mul0 = opts.parsed_synthesize_options.should_split_mul;
  should_split_multiret0 = opts.parsed_synthesize_options.should_split_multiret;
  Coq__14.assembly_hints_lines = opts.assembly_hints_lines;
  widen_carry0 = opts.parsed_synthesize_options.widen_carry;
  widen_bytes0 = opts.parsed_synthesize_options.widen_bytes;
  Coq__15.error_on_unused_assembly_functions = opts.parsed_synthesize_options.error_on_unused_assembly_functions;
  Coq__16.ignore_unique_asm_names = opts.parsed_synthesize_options.ignore_unique_asm_names;
  Coq__17.assembly_conventions = opts.parsed_synthesize_options.assembly_conventions;
}

Last updated: Feb 02 2023 at 13:03 UTC