Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ltac2 compile error with Coq 8.19.2 #33

Open
aa755 opened this issue Sep 18, 2024 · 0 comments
Open

Ltac2 compile error with Coq 8.19.2 #33

aa755 opened this issue Sep 18, 2024 · 0 comments

Comments

@aa755
Copy link

aa755 commented Sep 18, 2024

abhishek@optiplex:~/work/coq/coq-of-python/CoqOfPython$ coqc --version
The Coq Proof Assistant, version 8.19.2
compiled with OCaml 5.2.0

abhishek@optiplex:~/work/coq/coq-of-python/CoqOfPython$ make -j10 -k
make -f CoqMakefile all
make[1]: Entering directory '/home/abhishek/work/coq/coq-of-python/CoqOfPython'
COQC ./RecordUpdate.v
File "./RecordUpdate.v", line 47, characters 16-27:
Error: This expression has type 'a array.
It is not a function and cannot be applied.

Line 47 is the 6th line in the snippet below (| _ => (ty, Array.empty ()) )

Ltac2 record_with_set_val (ty : constr) (record : constr)                                                                                                    |                                                                                                                                                              
  (field : constr) (val : constr) : constr :=                                                                                                                |                                                                                                                                                              
  let (h, args) :=                                                                                                                                           |                                                                                                                                                              
    match Constr.Unsafe.kind ty with                                                                                                                         |                                                                                                                                                              
    | Constr.Unsafe.App h args => (h, args)                                                                                                                  |                                                                                                                                                              
    | _ => (ty, Array.empty ())                                                                                                                              |                                                                                                                                                              
    end in                                                                                                                                                   |                                                                                                                                                              
  let ctor := constructor_of_record h in                                                                                                                     |                                                                                                                                                              
  let getters := List.map (fun getterRef =>                                                                                                                  |                                                                                                                                                              
    mkApp (Env.instantiate getterRef) args) (field_names ctor) in                                                                                            |                                                                                                                                                              
  let fields := List.map (fun getter =>                                                                                                                      |                                                                                                                                                              
    if Constr.equal getter field then val else '($getter $record)                                                                                            |                                                                                                                                                              
    ) getters in                                                                                                                                             |                                                                                                                                                              
  let res :=                                                                                                                                                 |                                                                                                                                                              
    mkApp (mkApp (Env.instantiate ctor) args) (Array.of_list fields) in                                                                                      |                                                                                                                                                              
  res.   

Which Coq version should I use?

abhishek@optiplex:~/work/coq/coq-of-python/CoqOfPython$ opam list
# Packages matching: installed
# Name                  # Installed # Synopsis
base                    v0.17.1     Full standard library replacement for OCaml
base-bigarray           base
base-domains            base
base-nnp                base        Naked pointers prohibited in the OCaml heap
base-threads            base
base-unix               base
cerberus                dev         pinned to version dev at git+https://github.com/rems-project/cerberus.git#57c0e80af140651aad72e3514133229425aeb102
cerberus-lib            dev         pinned to version dev at git+https://github.com/rems-project/cerberus.git#57c0e80af140651aad72e3514133229425aeb102
cmdliner                1.3.0       Declarative definition of command line interfaces for OCaml
conf-c++                1.0         Virtual package relying on the c++ compiler
conf-findutils          1           Virtual package relying on findutils
conf-g++                1.0         Virtual package relying on the g++ compiler (for C++)
conf-gmp                4           Virtual package relying on a GMP lib system installation
conf-linux-libc-dev     0           Virtual package relying on the installation of the Linux kernel headers files
conf-pkg-config         3           Check if pkg-config is installed and create an opam switch local pkgconfig folder
conf-python-3           9.0.0       Virtual package relying on Python-3 installation
coq                     8.19.2      The Coq Proof Assistant
coq-core                8.19.2      The Coq Proof Assistant -- Core Binaries and Tools
coq-hammer              1.3.2+8.19  General-purpose automated reasoning hammer tool for Coq
coq-hammer-tactics      1.3.2+8.19  Reconstruction tactics for the hammer for Coq
coq-iris                4.2.0       A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-record-update       0.3.4       Generic support for updating record fields in Coq
coq-stdlib              8.19.2      The Coq Proof Assistant -- Standard Library
coq-stdpp               1.10.0      An extended "Standard Library" for Coq
coqide-server           8.19.2      The Coq Proof Assistant, XML protocol server
cppo                    1.7.0       Code preprocessor like cpp for OCaml
csexp                   1.5.2       Parsing and printing of S-expressions in Canonical form
dune                    3.16.0      Fast, portable, and opinionated build system
dune-configurator       3.16.0      Helper library for gathering system configuration
host-arch-x86_64        1           OCaml on amd64 (64-bit)
host-system-other       1           OCaml on an unidentified system
lem                     2022-12-10  Lem is a tool for lightweight executable mathematics
menhir                  20240715    An LR(1) parser generator
menhirCST               20240715    Runtime support library for parsers generated by Menhir
menhirLib               20240715    Runtime support library for parsers generated by Menhir
menhirSdk               20240715    Compile-time library for auxiliary tools related to Menhir
num                     1.5-1       The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                   5.2.0       The OCaml compiler (virtual package)
ocaml-base-compiler     5.2.0       Official release 5.2.0
ocaml-compiler-libs     v0.17.0     OCaml compiler libraries repackaged
ocaml-config            3           OCaml Switch Configuration
ocaml-options-vanilla   1           Ensure that OCaml is compiled with no special options enabled
ocaml_intrinsics_kernel v0.17.1     Intrinsics
ocamlbuild              0.15.0      OCamlbuild is a build system with builtin rules to easily build most OCaml projects
ocamlfind               1.9.6       A library manager for OCaml
parsexp                 v0.17.0     S-expression parsing library
pprint                  20230830    A pretty-printing combinator library and rendering engine
ppx_derivers            1.2.1       Shared [@@deriving] plugin registry
ppx_deriving            6.0.2       Type-driven code generation for OCaml
ppx_sexp_conv           v0.17.0     [@@deriving] plugin to generate S-expression conversion functions
ppxlib                  0.33.0      Standard infrastructure for ppx rewriters
ppxlib_jane             v0.17.0     Utilities for working with Jane Street AST constructs
result                  1.5         Compatibility Result module
seq                     base        Compatibility package for OCaml's standard iterator type starting from 4.07.
sexplib                 v0.17.0     Library for serializing OCaml values to and from S-expressions
sexplib0                v0.17.0     Library containing the definition of S-expressions and some base converters
sha                     1.15.4      Binding to the SHA cryptographic functions
stdlib-shims            0.3.0       Backport some of the new stdlib features to older compiler
yojson                  2.2.2       Yojson is an optimized parsing and printing library for the JSON format
z3                      4.13.0-3    Z3 solver
zarith                  1.14        Implements arithmetic and logical operations over arbitrary-precision integers
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant