diff options
40 files changed, 1574 insertions, 285 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 8dbdf43e52..c4d202470d 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -23,6 +23,7 @@ /dev/ci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers +/.github/workflows @coq/ci-maintainers /azure-pipelines.yml @coq/ci-maintainers /Makefile.ci @coq/ci-maintainers diff --git a/.github/workflows/check-conflicts.yml b/.github/workflows/check-conflicts.yml new file mode 100644 index 0000000000..33ed944488 --- /dev/null +++ b/.github/workflows/check-conflicts.yml @@ -0,0 +1,13 @@ +name: "Check conflicts" +on: [push] +# Only on push because @coqbot already takes care of checking for +# conflicts when PRs are opened or synchronized + +jobs: + main: + runs-on: ubuntu-latest + steps: + - uses: eps1lon/actions-label-merge-conflict@b8bf8341285ec9a4567d4318ba474fee998a6919 + with: + dirtyLabel: "needs: rebase" + repoToken: "${{ secrets.GITHUB_TOKEN }}" diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 32b05ec746..ed944366f1 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -927,3 +927,35 @@ plugin:ci-rewriter: name: "$CI_JOB_NAME" paths: - _build_ci + +bench: + stage: stage-1 + when: manual + before_script: + - printenv -0 | sort -z | tr '\0' '\n' + script: + - . ~/.opam/opam-init/init.sh + - ./dev/bench/gitlab.sh + tags: + - timing + variables: + coq_pr_number: "" + coq_pr_comment_id: "" + new_ocaml_switch: "ocaml-base-compiler.4.07.1" + old_ocaml_switch: "ocaml-base-compiler.4.07.1" + new_coq_repository: "https://gitlab.com/coq/coq.git" + old_coq_repository: "https://gitlab.com/coq/coq.git" + new_coq_commit: "$CI_COMMIT_SHA" + old_coq_commit: "master" + new_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" + old_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" + new_coq_opam_archive_git_branch: "master" + old_coq_opam_archive_git_branch: "master" + num_of_iterations: 1 + coq_opam_packages: "coq-performance-tests coq-engine-bench coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast" + artifacts: + name: "$CI_JOB_NAME" + paths: + - _bench/html/**/*.v.html + when: always + expire_in: 1 year diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh new file mode 100755 index 0000000000..5423f30aba --- /dev/null +++ b/dev/bench/gitlab.sh @@ -0,0 +1,510 @@ +#! /usr/bin/env bash + +# ASSUMPTIONS: +# - the OPAM packages, specified by the user, are topologically sorted wrt. to the dependency relationship. +# - all the variables below are set. + +set -e + +BENCH_DEBUG=1 + +r='\033[0m' # reset (all attributes off) +b='\033[1m' # bold +u='\033[4m' # underline +nl=$'\n' + +number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l) + +program_name="$0" +program_path=$(readlink -f "${program_name%/*}") + +coqbot_url_prefix="https://coqbot.herokuapp.com/pendulum/" + +# Check that the required arguments are provided + +check_variable () { + if [ ! -v "$1" ] + then + echo "Variable $1 should be set" + exit 1 + fi +} + +echo $PWD + +#check_variable "BUILD_ID" +#check_variable "BUILD_URL" +#check_variable "JOB_NAME" +#check_variable "JENKINS_URL" +check_variable "coq_pr_number" +check_variable "coq_pr_comment_id" +check_variable "new_ocaml_switch" +check_variable "new_coq_repository" +check_variable "new_coq_commit" +check_variable "new_coq_opam_archive_git_uri" +check_variable "new_coq_opam_archive_git_branch" +check_variable "old_ocaml_switch" +check_variable "old_coq_repository" +old_coq_commit="609152467f4d717713b7ea700f5155fc9f341cd7" +check_variable "old_coq_opam_archive_git_uri" +check_variable "old_coq_opam_archive_git_branch" +check_variable "num_of_iterations" +check_variable "coq_opam_packages" + +if which jq > /dev/null; then + : +else + echo > /dev/stderr + echo "ERROR: \"jq\" program is not available." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + +if echo "$num_of_iterations" | grep '^[1-9][0-9]*$' 2> /dev/null > /dev/null; then + : +else + echo + echo "ERROR: num_of_iterations \"$num_of_iterations\" is not a positive integer." > /dev/stderr + print_man_page_hint + exit 1 +fi + +mkdir -p "_bench" +working_dir="$PWD/_bench" + +log_dir=$working_dir/logs +mkdir "$log_dir" + +if [ ! -z "${coq_pr_number}" ]; then + github_response="$(curl "https://api.github.com/repos/coq/coq/pulls/${coq_pr_number}")" + new_coq_repository="$(echo "${github_response}" | jq -r '.head.repo.clone_url')" + new_coq_commit="$(echo "${github_response}" | jq -r '.head.sha')" + old_coq_repository="$(echo "${github_response}" | jq -r '.base.repo.clone_url')" + old_coq_commit="$(echo "${github_response}" | jq -r '.base.sha')" + coq_pr_title="$(echo "${github_response}" | jq -r '.title')" + # for coqbot parsing purposes, coq_pr_number and coq_pr_comment_id must not have newlines + coq_pr_number="$(echo "${coq_pr_number}" | tr -d '\n' | tr -d '\r')" + coq_pr_comment_id="$(echo "${coq_pr_comment_id}" | tr -d '\n' | tr -d '\r')" + + for val in "${new_coq_repository}" "${new_coq_commit}" "${old_coq_repository}" "${old_coq_commit}" "${coq_pr_title}"; do + if [ -z "$val" ] || [ "val" == "null" ]; then + echo 'ERROR: Invalid Response:' > /dev/stderr + echo "${github_response}" > /dev/stderr + echo "Info:" > /dev/stderr + curl -i "https://api.github.com/repos/coq/coq/pulls/${coq_pr_number}" > /dev/stderr + exit 1 + fi + done + + if [ -z "$BENCH_DEBUG" ]; then # if it's non-empty, this'll get + # printed later anyway. But we + # want to see it always if we're + # automatically computing values + echo "DEBUG: new_coq_repository = $new_coq_repository" + echo "DEBUG: new_coq_commit = $new_coq_commit" + echo "DEBUG: old_coq_repository = $old_coq_repository" + echo "DEBUG: old_coq_commit = $old_coq_commit" + fi + +fi + +if [ ! -z "$BENCH_DEBUG" ] +then + echo "DEBUG: ocaml -version = `ocaml -version`" + echo "DEBUG: working_dir = $working_dir" + echo "DEBUG: new_ocaml_switch = $new_ocaml_switch" + echo "DEBUG: new_coq_repository = $new_coq_repository" + echo "DEBUG: new_coq_commit = $new_coq_commit" + echo "DEBUG: new_coq_opam_archive_git_uri = $new_coq_opam_archive_git_uri" + echo "DEBUG: new_coq_opam_archive_git_branch = $new_coq_opam_archive_git_branch" + echo "DEBUG: old_ocaml_switch = $old_ocaml_switch" + echo "DEBUG: old_coq_repository = $old_coq_repository" + echo "DEBUG: old_coq_commit = $old_coq_commit" + echo "DEBUG: old_coq_opam_archive_git_uri = $old_coq_opam_archive_git_uri" + echo "DEBUG: old_coq_opam_archive_git_branch = $old_coq_opam_archive_git_branch" + echo "DEBUG: num_of_iterations = $num_of_iterations" + echo "DEBUG: coq_opam_packages = $coq_opam_packages" + echo "DEBUG: coq_pr_number = $coq_pr_number" + echo "DEBUG: coq_pr_comment_id = $coq_pr_comment_id" +fi + +# -------------------------------------------------------------------------------- + +# Some sanity checks of command-line arguments provided by the user that can be done right now. + +if which perf > /dev/null; then + echo -n +else + echo > /dev/stderr + echo "ERROR: \"perf\" program is not available." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + +if which curl > /dev/null; then + : +else + echo > /dev/stderr + echo "ERROR: \"curl\" program is not available." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + +if [ ! -e "$working_dir" ]; then + echo > /dev/stderr + echo "ERROR: \"$working_dir\" does not exist." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + +if [ ! -d "$working_dir" ]; then + echo > /dev/stderr + echo "ERROR: \"$working_dir\" is not a directory." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + +if [ ! -w "$working_dir" ]; then + echo > /dev/stderr + echo "ERROR: \"$working_dir\" is not writable." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + +coq_opam_packages_on_separate_lines=$(echo "$coq_opam_packages" | sed 's/ /\n/g') +if [ $(echo "$coq_opam_packages_on_separate_lines" | wc -l) != $(echo "$coq_opam_packages_on_separate_lines" | sort | uniq | wc -l) ]; then + echo "ERROR: The provided set of OPAM packages contains duplicates." + exit 1 +fi + +# -------------------------------------------------------------------------------- + +# Tell coqbot to update the initial comment, if we know which one to update +function coqbot_update_comment() { + is_done="$1" + comment_body="$2" + uninstallable_packages="$3" + + if [ ! -z "${coq_pr_number}" ]; then + comment_text="" + + if [ -z "${is_done}" ]; then + comment_text="in progress, " + else + comment_text="" + fi + comment_text="Benchmarking ${comment_text}log available [here](${BUILD_URL}/console), workspace available [here](${JENKINS_URL}/view/benchmarking/job/${JOB_NAME}/ws/${BUILD_ID})" + + if [ ! -z "${comment_body}" ]; then + comment_text="${comment_text}${nl}"'```'"${nl}${comment_body}${nl}"'```' + fi + + if [ ! -z "${uninstallable_packages}" ]; then + comment_text="${comment_text}${nl}The following packages failed to install: ${uninstallable_packages}" + fi + + # if there's a comment id, we update the comment while we're + # in progress; otherwise, we wait until the end to post a new + # comment + if [ ! -z "${coq_pr_comment_id}" ]; then + # Tell coqbot to update the in-progress comment + curl -X POST --data-binary "${coq_pr_number}${nl}${coq_pr_comment_id}${nl}${comment_text}" "${coqbot_url_prefix}/update-comment" + elif [ ! -z "${is_done}" ]; then + # Tell coqbot to post a new comment that we're done benchmarking + curl -X POST --data-binary "${coq_pr_number}${nl}${comment_text}" "${coqbot_url_prefix}/new-comment" + fi + if [ ! -z "${is_done}" ]; then + # Tell coqbot to remove the `needs: benchmarking` label + curl -X POST --data-binary "${coq_pr_number}" "${coqbot_url_prefix}/benchmarking-done" + fi + fi +} + +# initial update to the comment, to say that we're in progress +coqbot_update_comment "" "" "" + +# -------------------------------------------------------------------------------- + +# Clone the indicated git-repository. + +coq_dir="$working_dir/coq" +git clone -q "$new_coq_repository" "$coq_dir" +cd "$coq_dir" +git remote rename origin new_coq_repository +git remote add old_coq_repository "$old_coq_repository" +git fetch -q "$old_coq_repository" +git checkout -q $new_coq_commit + +official_coq_branch=master +coq_opam_version=dev + +# -------------------------------------------------------------------------------- + +new_opam_root="$working_dir/opam.NEW" +old_opam_root="$working_dir/opam.OLD" + +# -------------------------------------------------------------------------------- + +old_coq_opam_archive_dir="$working_dir/old_coq_opam_archive" +git clone -q --depth 1 -b "$old_coq_opam_archive_git_branch" "$old_coq_opam_archive_git_uri" "$old_coq_opam_archive_dir" +new_coq_opam_archive_dir="$working_dir/new_coq_opam_archive" +git clone -q --depth 1 -b "$new_coq_opam_archive_git_branch" "$new_coq_opam_archive_git_uri" "$new_coq_opam_archive_dir" + +initial_opam_packages="num ocamlfind dune" + +# Create an opam root and install Coq +# $1 = root_name {ex: NEW / OLD} +# $2 = compiler name +# $3 = git hash of Coq to be installed +# $4 = directory of coq opam archive +create_opam() { + + local RUNNER="$1" + local OPAM_DIR="$working_dir/opam.$RUNNER" + local OPAM_COMP="$2" + local COQ_HASH="$3" + local OPAM_COQ_DIR="$4" + + export OPAMROOT="$OPAM_DIR" + + opam init --disable-sandboxing -qn -j$number_of_processors --bare + # Allow beta compiler switches + opam repo add -q --set-default beta https://github.com/ocaml/ocaml-beta-repository.git + # Allow experimental compiler switches + opam repo add -q --set-default ocaml-pr https://github.com/ejgallego/ocaml-pr-repository.git + # Rest of default switches + opam repo add -q --set-default iris-dev "https://gitlab.mpi-sws.org/FP/opam-dev.git" + + opam switch create -qy -j$number_of_processors "$OPAM_COMP" + eval $(opam env) + + # For some reason opam guesses an incorrect upper bound on the + # number of jobs available on Travis, so we set it here manually: + opam config set-global jobs $number_of_processors + if [ ! -z "$BENCH_DEBUG" ]; then opam config list; fi + + opam repo add -q --this-switch coq-extra-dev "$OPAM_COQ_DIR/extra-dev" + opam repo add -q --this-switch coq-released "$OPAM_COQ_DIR/released" + + opam install -qy -j$number_of_processors $initial_opam_packages + if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi + + cd "$coq_dir" + if [ ! -z "$BENCH_DEBUG" ]; then echo "DEBUG: $1_coq_commit = $COQ_HASH"; fi + + git checkout -q $COQ_HASH + COQ_HASH_LONG=$(git log --pretty=%H | head -n 1) + + echo "$1_coq_commit_long = $COQ_HASH_LONG" + + _RES=0 + /usr/bin/time -o "$log_dir/coq.$RUNNER.1.time" --format="%U %M %F" \ + perf stat -e instructions:u,cycles:u -o "$log_dir/coq.$RUNNER.1.perf" \ + opam pin add -y -b -j "$number_of_processors" --kind=path coq.dev . \ + 3>$log_dir/coq.$RUNNER.opam_install.1.stdout 1>&3 \ + 4>$log_dir/coq.$RUNNER.opam_install.1.stderr 2>&4 || \ + _RES=$? + if [ $_RES = 0 ]; then + echo "Coq ($RUNNER) installed successfully" + else + echo "ERROR: \"opam install coq.$coq_opam_version\" has failed (for the $RUNNER commit = $COQ_HASH_LONG)." + exit 1 + fi + + # we don't multi compile coq for now (TODO some other time) + # the render needs all the files so copy them around + for it in $(seq 2 $num_of_iterations); do + cp "$log_dir/coq.$RUNNER.1.time" "$log_dir/coq.$RUNNER.$it.time" + cp "$log_dir/coq.$RUNNER.1.perf" "$log_dir/coq.$RUNNER.$it.perf" + done + +} + +# Create an OPAM-root to which we will install the NEW version of Coq. +create_opam "NEW" "$new_ocaml_switch" "$new_coq_commit" "$new_coq_opam_archive_dir" +new_coq_commit_long="$COQ_HASH_LONG" + +# Create an OPAM-root to which we will install the OLD version of Coq. +create_opam "OLD" "$old_ocaml_switch" "$old_coq_commit" "$old_coq_opam_archive_dir" +old_coq_commit_long="$COQ_HASH_LONG" +# -------------------------------------------------------------------------------- +# Measure the compilation times of the specified OPAM packages in both switches + +# Sort the opam packages +sorted_coq_opam_packages=$("${program_path}/sort-by-deps.sh" ${coq_opam_packages}) +if [ ! -z "$BENCH_DEBUG" ] +then + echo "DEBUG: sorted_coq_opam_packages = ${sorted_coq_opam_packages}" +fi + +# Generate per line timing info in devs that use coq_makefile +export TIMING=1 + +# The following variable will be set in the following cycle: +installable_coq_opam_packages=coq + +for coq_opam_package in $sorted_coq_opam_packages; do + + if [ ! -z "$BENCH_DEBUG" ]; then + opam list + echo "DEBUG: coq_opam_package = $coq_opam_package" + opam show $coq_opam_package || continue 2 + else + # cause to skip with error if unknown package + opam show $coq_opam_package >/dev/null || continue 2 + fi + + for RUNNER in NEW OLD; do + + # perform measurements for the NEW/OLD commit (provided by the user) + if [ $RUNNER = "NEW" ]; then + export OPAMROOT="$new_opam_root" + echo "Testing NEW commit: $(date)" + else + export OPAMROOT="$old_opam_root" + echo "Testing OLD commit: $(date)" + fi + + eval $(opam env) + + # If a given OPAM-package was already installed (as a + # dependency of some OPAM-package that we have benchmarked + # before), remove it. + opam uninstall -q $coq_opam_package + + # OPAM 2.0 likes to ignore the -j when it feels like :S so we + # workaround that here. + opam config set-global jobs $number_of_processors + + opam install $coq_opam_package -v -b -j$number_of_processors --deps-only -y \ + 3>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stdout 1>&3 \ + 4>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stderr 2>&4 || continue 2 + + opam config set-global jobs 1 + + if [ ! -z "$BENCH_DEBUG" ]; then ls -l $working_dir; fi + + for iteration in $(seq $num_of_iterations); do + _RES=0 + /usr/bin/time -o "$log_dir/$coq_opam_package.$RUNNER.$iteration.time" --format="%U %M %F" \ + perf stat -e instructions:u,cycles:u -o "$log_dir/$coq_opam_package.$RUNNER.$iteration.perf" \ + opam install -v -b -j1 $coq_opam_package \ + 3>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stdout 1>&3 \ + 4>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stderr 2>&4 || \ + _RES=$? + if [ $_RES = 0 ]; + then + echo $_RES > $log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.exit_status + # "opam install" was successful. + + # Remove the benchmarked OPAM-package, unless this is the + # very last iteration (we want to keep this OPAM-package + # because other OPAM-packages we will benchmark later + # might depend on it --- it would be a waste of time to + # remove it now just to install it later) + if [ $iteration != $num_of_iterations ]; then + opam uninstall -q $coq_opam_package + fi + else + # "opam install" failed. + echo $_RES > $log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.exit_status + continue 3 + fi + done + done + + installable_coq_opam_packages="$installable_coq_opam_packages $coq_opam_package" + + # -------------------------------------------------------------- + + # Print the intermediate results after we finish benchmarking each OPAM package + if [ "$coq_opam_package" = "$(echo $sorted_coq_opam_packages | sed 's/ /\n/g' | tail -n 1)" ]; then + + # It does not make sense to print the intermediate results when + # we finished bechmarking the very last OPAM package because the + # next thing will do is that we will print the final results. + # It would look lame to print the same table twice. + : + else + + echo "DEBUG: $program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages" + if [ ! -z "$BENCH_DEBUG" ]; then + cat $log_dir/$coq_opam_package.$RUNNER.1.time || true + cat $log_dir/$coq_opam_package.$RUNNER.1.perf || true + fi + rendered_results="$($program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages)" + echo "${rendered_results}" + # update the comment + coqbot_update_comment "" "${rendered_results}" "" + fi + + # Generate HTML report for LAST run + + # N.B. Not all packages end in .dev, e.g., coq-lambda-rust uses .dev.timestamp. + # So we use a wildcard to catch such packages. This will have to be updated if + # ever there is a package that uses some different naming scheme. + new_base_path=$new_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ + old_base_path=$old_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ + for vo in `cd $new_opam_root/$new_base_path/; find -name '*.vo'`; do + if [ -e $old_opam_root/$old_base_path/${vo%%o}.timing -a \ + -e $new_opam_root/$new_base_path/${vo%%o}.timing ]; then + mkdir -p $working_dir/html/$coq_opam_package/`dirname $vo`/ + $program_path/timelog2html $new_opam_root/$new_base_path/${vo%%o} \ + $old_opam_root/$old_base_path/${vo%%o}.timing \ + $new_opam_root/$new_base_path/${vo%%o}.timing > \ + $working_dir/html/$coq_opam_package/${vo%%o}.html + fi + done +done + +# The following directories in $working_dir are no longer used: +# +# - coq, opam.OLD, opam.NEW + +# Measured data for each `$coq_opam_package`, `$iteration`, `status \in {NEW,OLD}`: +# +# - $working_dir/$coq_opam_package.$status.$iteration.time +# => output of /usr/bin/time --format="%U" ... +# +# - $working_dir/$coq_opam_package.NEW.$iteration.perf +# => output of perf stat -e instructions:u,cycles:u ... +# +# The next script processes all these files and prints results in a table. + +echo "INFO: workspace = https://ci.inria.fr/coq/view/benchmarking/job/$JOB_NAME/ws/$BUILD_ID" + +# Print the final results. +if [ -z "$installable_coq_opam_packages" ]; then + # Tell the user that none of the OPAM-package(s) the user provided + # /are installable. + printf "\n\nINFO: failed to install: $sorted_coq_opam_packages" + coqbot_update_comment "done" "" "$sorted_coq_opam_packages" + exit 1 +else + echo "DEBUG: $program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages" + rendered_results="$($program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages)" + echo "${rendered_results}" + + echo "INFO: per line timing: https://ci.inria.fr/coq/job/$JOB_NAME/ws/$BUILD_ID/html/" + + cd "$coq_dir" + echo INFO: Old Coq version + git log -n 1 "$old_coq_commit" + echo INFO: New Coq version + git log -n 1 "$new_coq_commit" + + not_installable_coq_opam_packages=`comm -23 <(echo $sorted_coq_opam_packages | sed 's/ /\n/g' | sort | uniq) <(echo $installable_coq_opam_packages | sed 's/ /\n/g' | sort | uniq) | sed 's/\t//g'` + + coqbot_update_comment "done" "${rendered_results}" "${not_installable_coq_opam_packages}" + + exit_code=0 + + if [ ! -z "$not_installable_coq_opam_packages" ]; then + # Tell the user that some of the provided OPAM-package(s) + # is/are not installable. + printf '\n\nINFO: failed to install %s\n' "$not_installable_coq_opam_packages" + exit_code=1 + fi + + exit 0 +fi diff --git a/dev/bench/render_results b/dev/bench/render_results new file mode 100755 index 0000000000..72affd70b2 --- /dev/null +++ b/dev/bench/render_results @@ -0,0 +1,434 @@ +#! /usr/bin/env ocaml + +(* ASSUMPTIONS: + - the 1-st command line argument (working directory): + - designates an existing readable directory + - which contains *.time and *.perf files produced by bench.sh script + - the 2-nd command line argument (number of iterations): + - is a positive integer + - the 3-rd command line argument (minimal user time): + - is a positive floating point number + - the 4-th command line argument determines the name of the column according to which the resulting table will be sorted. + Valid values are: + - package_name + - user_time_pdiff + - the rest of the command line-arguments + - are names of benchamarked Coq OPAM packages for which bench.sh script generated *.time and *.perf files + *) + +#use "topfind";; +#require "unix";; +#print_depth 100000000;; +#print_length 100000000;; + +open Printf +open Unix +;; + +let _ = Printexc.record_backtrace true +;; + +type ('a,'b) pkg_timings = { + user_time : 'a; + num_instr : 'b; + num_cycles : 'b; + num_mem : 'b; + num_faults : 'b; +} +;; + +let reduce_pkg_timings (m_f : 'a list -> 'c) (m_a : 'b list -> 'd) (t : ('a,'b) pkg_timings list) : ('c,'d) pkg_timings = + { user_time = m_f @@ List.map (fun x -> x.user_time) t + ; num_instr = m_a @@ List.map (fun x -> x.num_instr) t + ; num_cycles = m_a @@ List.map (fun x -> x.num_cycles) t + ; num_mem = m_a @@ List.map (fun x -> x.num_mem) t + ; num_faults = m_a @@ List.map (fun x -> x.num_faults) t + } +;; + +(******************************************************************************) +(* BEGIN Copied from batteries, to remove *) +(******************************************************************************) +let run_and_read cmd = + (* This code is before the open of BatInnerIO + to avoid using batteries' wrapped IOs *) + let string_of_file fn = + let buff_size = 1024 in + let buff = Buffer.create buff_size in + let ic = open_in fn in + let line_buff = Bytes.create buff_size in + begin + let was_read = ref (input ic line_buff 0 buff_size) in + while !was_read <> 0 do + Buffer.add_subbytes buff line_buff 0 !was_read; + was_read := input ic line_buff 0 buff_size; + done; + close_in ic; + end; + Buffer.contents buff + in + let tmp_fn = Filename.temp_file "" "" in + let cmd_to_run = cmd ^ " > " ^ tmp_fn in + let status = Unix.system cmd_to_run in + let output = string_of_file tmp_fn in + Unix.unlink tmp_fn; + (status, output) +;; + +let ( %> ) f g x = g (f x) +;; + +let run = run_and_read %> snd +;; + +module Float = struct + let nan = Pervasives.nan +end + +module Tuple4 = struct + + let first (x,_,_,_) = x + let second (_,y,_,_) = y + let third (_,_,z,_) = z + let fourth (_,_,_,z) = z + +end +;; + +module List = struct + include List + + let rec init_tailrec_aux acc i n f = + if i >= n then acc + else init_tailrec_aux (f i :: acc) (i+1) n f + + let rec init_aux i n f = + if i >= n then [] + else + let r = f i in + r :: init_aux (i+1) n f + + let rev_init_threshold = + match Sys.backend_type with + | Sys.Native | Sys.Bytecode -> 10_000 + (* We don't known the size of the stack, better be safe and assume it's small. *) + | Sys.Other _ -> 50 + + let init len f = + if len < 0 then invalid_arg "List.init" else + if len > rev_init_threshold then rev (init_tailrec_aux [] 0 len f) + else init_aux 0 len f + + let rec drop n = function + | _ :: l when n > 0 -> drop (n-1) l + | l -> l + + let reduce f = function + | [] -> + invalid_arg "List.reduce: Empty List" + | h :: t -> + fold_left f h t + + let min l = reduce Pervasives.min l + let max l = reduce Pervasives.max l + +end +;; + +module String = struct + + include String + + let rchop ?(n = 1) s = + if n < 0 then + invalid_arg "String.rchop: number of characters to chop is negative" + else + let slen = length s in + if slen <= n then "" else sub s 0 (slen - n) + +end +;; + +(******************************************************************************) +(* END Copied from batteries, to remove *) +(******************************************************************************) + +let mk_pkg_timings work_dir pkg_name suffix iteration = + let command_prefix = "cat " ^ work_dir ^ "/" ^ pkg_name ^ suffix ^ string_of_int iteration in + let time_command_output = command_prefix ^ ".time" |> run |> String.rchop ~n:1 |> String.split_on_char ' ' in + + let nth x i = List.nth i x in + + { user_time = time_command_output |> nth 0 |> float_of_string + (* Perf can indeed be not supported in some systems, so we must fail gracefully *) + ; num_instr = + (try command_prefix ^ ".perf | grep instructions:u | awk '{print $1}' | sed 's/,//g'" |> + run |> String.rchop ~n:1 |> int_of_string + with Failure _ -> 0) + ; num_cycles = + (try command_prefix ^ ".perf | grep cycles:u | awk '{print $1}' | sed 's/,//g'" |> + run |> String.rchop ~n:1 |> int_of_string + with Failure _ -> 0) + ; num_mem = time_command_output |> nth 1 |> int_of_string + ; num_faults = time_command_output |> nth 2 |> int_of_string + } +;; + +(* process command line paramters *) +assert (Array.length Sys.argv > 5); +let work_dir = Sys.argv.(1) in +let num_of_iterations = int_of_string Sys.argv.(2) in +let new_coq_version = Sys.argv.(3) in +let old_coq_version = Sys.argv.(4) in +let minimal_user_time = float_of_string Sys.argv.(5) in +let sorting_column = Sys.argv.(6) in +let coq_opam_packages = Sys.argv |> Array.to_list |> List.drop 7 in + +(* ASSUMPTIONS: + + "working_dir" contains all the files produced by the following command: + + two_points_on_the_same_branch.sh $working_directory $coq_repository $coq_branch[:$new:$old] $num_of_iterations coq_opam_package_1 coq_opam_package_2 ... coq_opam_package_N +-sf +*) + +(* Run a given bash command; + wait until it termines; + check if its exit status is 0; + return its whole stdout as a string. *) + +let proportional_difference_of_integers new_value old_value = + if old_value = 0 + then Float.nan + else float_of_int (new_value - old_value) /. float_of_int old_value *. 100.0 +in + +let count_number_of_digits_before_decimal_point = + log10 %> floor %> int_of_float %> succ %> max 1 +in + +(* parse the *.time and *.perf files *) +coq_opam_packages +|> List.map + (fun package_name -> + package_name,(* compilation_results_for_NEW : (float * int * int * int) list *) + List.init num_of_iterations succ |> List.map (mk_pkg_timings work_dir package_name ".NEW."), + List.init num_of_iterations succ |> List.map (mk_pkg_timings work_dir package_name ".OLD.")) + +(* from the list of measured values, select just the minimal ones *) + +|> List.map + (fun ((package_name : string), + (new_measurements : (float, int) pkg_timings list), + (old_measurements : (float, int) pkg_timings list)) -> + let f_min : float list -> float = List.min in + let i_min : int list -> int = List.min in + package_name, + reduce_pkg_timings f_min i_min new_measurements, + reduce_pkg_timings f_min i_min old_measurements + ) + +(* compute the "proportional differences in % of the NEW measurement and the OLD measurement" of all measured values *) +|> List.map + (fun (package_name, new_t, old_t) -> + package_name, new_t, old_t, + { user_time = (new_t.user_time -. old_t.user_time) /. old_t.user_time *. 100.0 + ; num_instr = proportional_difference_of_integers new_t.num_instr old_t.num_instr + ; num_cycles = proportional_difference_of_integers new_t.num_cycles old_t.num_cycles + ; num_mem = proportional_difference_of_integers new_t.num_mem old_t.num_mem + ; num_faults = proportional_difference_of_integers new_t.num_faults old_t.num_faults + }) + +(* sort the table with results *) +|> List.sort + (match sorting_column with + | "user_time_pdiff" -> + fun (_,_,_,perf1) (_,_,_,perf2) -> + compare perf1.user_time perf2.user_time + | "package_name" -> + fun (n1,_,_,_) (n2,_,_,_) -> compare n1 n2 + | _ -> + assert false + ) + +(* Keep only measurements that took at least "minimal_user_time" (in seconds). *) + +|> List.filter + (fun (_, new_t, old_t, _) -> + minimal_user_time <= new_t.user_time && minimal_user_time <= old_t.user_time) + +(* Below we take the measurements and format them to stdout. *) + +|> fun measurements -> + + let precision = 2 in + + (* the labels that we will print *) + let package_name__label = "package_name" in + let new__label = "NEW" in + let old__label = "OLD" in + let proportional_difference__label = "PDIFF" in + + (* the lengths of labels that we will print *) + let new__label__length = String.length new__label in + let proportional_difference__label__length = String.length proportional_difference__label in + + (* widths of individual columns of the table *) + let package_name__width = + max (measurements |> List.map (Tuple4.first %> String.length) |> List.max) + (String.length package_name__label) in + + let llf proj = + let lls = count_number_of_digits_before_decimal_point (List.max proj) + 1 + precision in + max lls new__label__length in + + let lli proj = + let lls = count_number_of_digits_before_decimal_point (float_of_int (List.(max proj))) + 1 + precision in + max lls new__label__length in + + let new_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.second measurements in + let old_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.third measurements in + + let llp proj = + let lls = + count_number_of_digits_before_decimal_point List.(max List.(map abs_float proj)) + 2 + precision in + max lls proportional_difference__label__length in + + let perc_timing_width = reduce_pkg_timings llp llp @@ List.map Tuple4.fourth measurements in + + (* print the table *) + let rec make_dashes = function + | 0 -> "" + | count -> "─" ^ make_dashes (pred count) + in + + let vertical_separator left_glyph middle_glyph right_glyph = + sprintf "%s─%s─%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s\n" + left_glyph + (make_dashes package_name__width) + middle_glyph + (make_dashes new_timing_width.user_time) + (make_dashes old_timing_width.user_time) + (make_dashes perc_timing_width.user_time) + middle_glyph + (make_dashes new_timing_width.num_cycles) + (make_dashes old_timing_width.num_cycles) + (make_dashes perc_timing_width.num_cycles) + middle_glyph + (make_dashes new_timing_width.num_instr) + (make_dashes old_timing_width.num_instr) + (make_dashes perc_timing_width.num_instr) + middle_glyph + (make_dashes new_timing_width.num_mem) + (make_dashes old_timing_width.num_mem) + (make_dashes perc_timing_width.num_mem) + middle_glyph + (make_dashes new_timing_width.num_faults) + (make_dashes old_timing_width.num_faults) + (make_dashes perc_timing_width.num_faults) + right_glyph + in + + let center_string string width = + let string_length = String.length string in + let width = max width string_length in + let left_hfill = (width - string_length) / 2 in + let right_hfill = width - left_hfill - string_length in + String.make left_hfill ' ' ^ string ^ String.make right_hfill ' ' + in + printf "\n"; + print_string (vertical_separator "┌" "┬" "┐"); + "│" ^ String.make (1 + package_name__width + 1) ' ' ^ "│" + ^ center_string "user time [s]" (1 + new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) ^ "│" + ^ center_string "CPU cycles" (1 + new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) ^ "│" + ^ center_string "CPU instructions" (1 + new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ^ "│" + ^ center_string "max resident mem [KB]" (1 + new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ^ "│" + ^ center_string "mem faults" (1 + new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) + ^ "│\n" |> print_string; + printf "│%*s │ %*s│ %*s│ %*s│ %*s│ %*s│\n" + (1 + package_name__width) "" + (new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) "" + (new_timing_width.num_cycles + 1 + old_timing_width.num_cycles + 1 + perc_timing_width.num_cycles + 3) "" + (new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) "" + (new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) "" + (new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) ""; + printf "│ %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │ %*s %*s %*s │\n" + package_name__width package_name__label + new_timing_width.user_time new__label + old_timing_width.user_time old__label + perc_timing_width.user_time proportional_difference__label + new_timing_width.num_cycles new__label + old_timing_width.num_cycles old__label + perc_timing_width.num_cycles proportional_difference__label + new_timing_width.num_instr new__label + old_timing_width.num_instr old__label + perc_timing_width.num_instr proportional_difference__label + new_timing_width.num_mem new__label + old_timing_width.num_mem old__label + perc_timing_width.num_mem proportional_difference__label + new_timing_width.num_faults new__label + old_timing_width.num_faults old__label + perc_timing_width.num_faults proportional_difference__label; + measurements |> List.iter + (fun (package_name, new_t, old_t, perc) -> + print_string (vertical_separator "├" "┼" "┤"); + printf "│ %*s │ %*.*f %*.*f %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │\n" + package_name__width package_name + new_timing_width.user_time precision new_t.user_time + old_timing_width.user_time precision old_t.user_time + perc_timing_width.user_time precision perc.user_time + new_timing_width.num_cycles new_t.num_cycles + old_timing_width.num_cycles old_t.num_cycles + perc_timing_width.num_cycles precision perc.num_cycles + new_timing_width.num_instr new_t.num_instr + old_timing_width.num_instr old_t.num_instr + perc_timing_width.num_instr precision perc.num_instr + new_timing_width.num_mem new_t.num_mem + old_timing_width.num_mem old_t.num_mem + perc_timing_width.num_mem precision perc.num_mem + new_timing_width.num_faults new_t.num_faults + old_timing_width.num_faults old_t.num_faults + perc_timing_width.num_faults precision perc.num_faults); + +print_string (vertical_separator "└" "┴" "┘"); + +(* ejgallego: disable this as it is very verbose and brings up little info in the log. *) +if false then begin +printf " + +PDIFF = proportional difference between measurements done for the NEW and the OLD Coq version + = (NEW_measurement - OLD_measurement) / OLD_measurement * 100%% + +NEW = %s +OLD = %s + +Columns: + + 1. user time [s] + + Total number of CPU-seconds that the process used directly (in user mode), in seconds. + (In other words, \"%%U\" quantity provided by the \"/usr/bin/time\" command.) + + 2. CPU cycles + + Total number of CPU-cycles that the process used directly (in user mode). + (In other words, \"cycles:u\" quantity provided by the \"/usr/bin/perf\" command.) + + 3. CPU instructions + + Total number of CPU-instructions that the process used directly (in user mode). + (In other words, \"instructions:u\" quantity provided by the \"/usr/bin/perf\" command.) + + 4. max resident mem [KB] + + Maximum resident set size of the process during its lifetime, in Kilobytes. + (In other words, \"%%M\" quantity provided by the \"/usr/bin/time\" command.) + + 5. mem faults + + Number of major, or I/O-requiring, page faults that occurred while the process was running. + These are faults where the page has actually migrated out of primary memory. + (In other words, \"%%F\" quantity provided by the \"/usr/bin/time\" command.) + +" new_coq_version old_coq_version; +end diff --git a/dev/bench/sort-by-deps b/dev/bench/sort-by-deps new file mode 100644 index 0000000000..e1da4e0ed5 --- /dev/null +++ b/dev/bench/sort-by-deps @@ -0,0 +1,33 @@ +#!/usr/bin/env ocaml + +let get_pkg_name arg = + List.nth (String.split_on_char ':' arg) 0 + +let get_pkg_deps arg = + String.split_on_char ',' (List.nth (String.split_on_char ':' arg) 1) + +let split_pkg arg = get_pkg_name arg, get_pkg_deps arg + +let depends_on arg1 arg2 = + let pkg1, deps1 = split_pkg arg1 in + let pkg2, deps2 = split_pkg arg2 in + pkg1 != pkg2 && List.mem pkg2 deps1 + +let rec sort = function + | [], [] -> [] + | [], deferred -> sort (List.rev deferred, []) + | arg :: rest, deferred -> + (* check if any remaining package reverse-depends on this one *) + if List.exists (fun other_arg -> depends_on arg other_arg) rest + then (* defer this package *) + sort (rest, arg :: deferred) + else (* emit this package, and then try again with any deferred packages *) + arg :: sort (List.rev deferred @ rest, []) + +let main () = + let args = Array.to_list Sys.argv in + let pkgs = List.tl args in + let sorted_pkgs = sort (pkgs, []) in + Printf.printf "%s\n%!" (String.concat " " (List.map get_pkg_name sorted_pkgs)) + +let () = main () diff --git a/dev/bench/sort-by-deps.sh b/dev/bench/sort-by-deps.sh new file mode 100755 index 0000000000..075976c17d --- /dev/null +++ b/dev/bench/sort-by-deps.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash + +program_name="$0" +program_path=$(readlink -f "${program_name%/*}") + +# We add || true (which may not be needed without set -e) to be +# explicit about the fact that this script does not fail even if `opam +# install --show-actions` does, e.g., because of a non-existent +# package +# +# TODO: Figure out how to use the OPAM API +# (https://opam.ocaml.org/doc/api/) to call this from OCaml. +for i in "$@"; do + echo -n "$i:"; ((echo -n "$(opam install --show-actions "$i" | grep -o '∗\s*install\s*[^ ]*' | sed 's/∗\s*install\s*//g')" | tr '\n' ',') || true); echo +done | xargs ocaml "${program_path}/sort-by-deps" diff --git a/dev/bench/timelog2html b/dev/bench/timelog2html new file mode 100755 index 0000000000..abbeb5936d --- /dev/null +++ b/dev/bench/timelog2html @@ -0,0 +1,141 @@ +#!/usr/bin/env lua5.1 + +args = {...} + +vfile = assert(args[1], "arg1 missing: .v file") +table.remove(args,1) +assert(#args > 0, "arg missing: at lease one aux file") +data_files = args + +source = assert(io.open(vfile), "unable to open "..vfile):read("*a") + +function htmlescape(s) + return (s:gsub("&","&"):gsub("<","<"):gsub(">",">")) +end + +colors = { + '#F08080', '#EEE8AA', '#98FB98' +} + +assert(#data_files <= #colors, "only ".. #colors .." data files are supported") + +vname = vfile:match("([^/]+.v)$") + +print([[ +<html> +<head> +<title>]]..vname..[[</title> +<style>]]) +for i,k in ipairs(colors) do + print( + ".time" .. i .. " {".. + "background-color: " .. k .. ";".. + "height: ".. 100 / #data_files .."%;".. + "top: " .. 100 / #data_files * (i - 1) .. "%;".. + "z-index: -1; position: absolute; opacity: 50%; }") +end +print([[.code { + z-index: 0; + position: relative; + border-style: solid; + border-color: transparent; + border-width: 1px; +} +.code:hover { + border-color: black; +} +pre { + display: inline; +} +</style> +</head> +<body> +<h1>Timings for ]]..vname..[[</h1> +<ol> +]]) +for i,data_file in ipairs(data_files) do + print('<li style="background-color: '..colors[i]..'">' .. data_file .. "</li>") +end +print("</ol>") + +all_data = {} + +for _, data_file in ipairs(data_files) do + local data = {} + local last_end = -1 + local lines = 1 + for l in io.lines(data_file) do + local b,e,t = l:match('^Chars ([%d]+) %- ([%d]+) %S+ ([%d%.]+) secs') + if b then + if tonumber(b) > last_end + 1 then + local text = string.sub(source,last_end+1,b-1) + if not text:match('^%s+$') then + local _, n = text:gsub('\n','') + data[#data+1] = { + start = last_end+1; stop = b-1; time = 0; + text = text; lines = lines + } + lines = lines + n + last_end = b + end + end + local text = string.sub(source,last_end+1,e) + local _, n = text:gsub('\n','') + local _, eoln = text:match('^[%s\n]*'):gsub('\n','') + data[#data+1] = { + start = b; stop = e; time = tonumber(t); text = text; + lines = lines + } + lines = lines + n + last_end = tonumber(e) + end + end + if last_end + 1 <= string.len(source) then + local text = string.sub(source,last_end+1,string.len(source)) + data[#data+1] = { + start = last_end+1; stop = string.len(source); time = 0; + text = text; lines = lines+1 + } + end +all_data[#all_data+1] = data +end + +max = 0; +for _, data in ipairs(all_data) do + for _,d in ipairs(data) do + max = math.max(max,d.time) + end +end + +data = all_data[1] +for j,d in ipairs(data) do + print('<div class="code" title="File: '..vname.. + '\nLine: '..d.lines..'\n') + for k=1,#all_data do + print('Time'..k..': '..all_data[k][j].time..'s') + end + print('">') + for k=1,#all_data do + print('<div class="time'..k..'" style="width: '.. + all_data[k][j].time * 100 / max ..'%"></div>') + end + if d.text == '\n' then + print('<pre>\n\n</pre>') + elseif d.text:match('\n$') then + print('<pre>'..htmlescape(d.text)..'\n</pre>') + else + print('<pre>'..htmlescape(d.text)..'</pre>') + end + print("</div>") +end + +print [[ +</body> +</html> +]] + +-- vim: set ts=4: + +--for i = 1,#data do +-- io.stderr:write(data[i].text) +--end diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh new file mode 100644 index 0000000000..54fdd87566 --- /dev/null +++ b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then + + mathcomp_CI_REF=dont-refresh-argument-names-overlay + mathcomp_CI_GITURL=https://github.com/jashug/math-comp + + oddorder_CI_REF=dont-refresh-argument-names-overlay + oddorder_CI_GITURL=https://github.com/jashug/odd-order + +fi diff --git a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst new file mode 100644 index 0000000000..b0cf4ca4e3 --- /dev/null +++ b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst @@ -0,0 +1,9 @@ +- **Changed:** + Tweaked the algorithm giving default names to arguments. + Should reduce the frequency that argument names get an + unexpected suffix. + Also makes :flag:`Mangle Names` not mess up argument names. + (`#12756 <https://github.com/coq/coq/pull/12756>`_, + fixes `#12001 <https://github.com/coq/coq/issues/12001>`_ + and `#6785 <https://github.com/coq/coq/issues/6785>`_, + by Jasper Hugunin). diff --git a/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst b/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst new file mode 100644 index 0000000000..289d17167d --- /dev/null +++ b/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Anomaly with :tacn:`injection` involving artificial + dependencies disappearing by reduction + (`#12816 <https://github.com/coq/coq/pull/12816>`_, + fixes `#12787 <https://github.com/coq/coq/issues/12787>`_, + by Hugo Herbelin). diff --git a/interp/impargs.ml b/interp/impargs.ml index db102470b0..48961c6c8a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -20,7 +20,6 @@ open Lib open Libobject open EConstr open Reductionops -open Namegen open Constrexpr module NamedDecl = Context.Named.Declaration @@ -247,24 +246,15 @@ let is_rigid env sigma t = is_rigid_head sigma t | _ -> true -let find_displayed_name_in sigma all avoid na (env, b) = - let envnames_b = (env, b) in - let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in sigma flag avoid na b - else compute_displayed_name_in sigma flag avoid na b - -let compute_implicits_names_gen all env sigma t = +let compute_implicits_names env sigma t = let open Context.Rel.Declaration in - let rec aux env avoid names t = + let rec aux env names t = let t = whd_all env sigma t in match kind sigma t with | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in - aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b + aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b | _ -> List.rev names - in aux env Id.Set.empty [] t - -let compute_implicits_names = compute_implicits_names_gen true + in aux env [] t let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t = let open Context.Rel.Declaration in @@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t = (f.strict || f.strongly_strict) f.strongly_strict f.reversible_pattern f.contextual env sigma t -let compute_implicits_flags env sigma f all t = +let compute_implicits_flags env sigma f t = List.combine - (compute_implicits_names_gen all env sigma t) + (compute_implicits_names env sigma t) (compute_implicits_explanation_flags env sigma f t) let compute_auto_implicits env sigma flags enriching t = @@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) = let rec prepare_implicits i f = function | [] -> [] - | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") - | (Name id, Some imp)::imps -> + | (na, Some imp)::imps -> let imps' = prepare_implicits (i+1) f imps in - Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps' + let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in + Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits (i+1) f imps let set_manual_implicits silent flags enriching autoimps l = @@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l = let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] - else let l = compute_implicits_flags env sigma f false t in + else let l = compute_implicits_flags env sigma f t in [DefaultImpArgs, prepare_implicits 1 f l] (*s Constants. *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 4a41f4c890..d215a7673d 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -604,6 +604,13 @@ let pp_global k r = | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) +(* Main name printing function for declaring a reference *) + +let pp_global_name k r = + let ls = ref_renaming (k,r) in + assert (List.length ls > 1); + List.hd ls + (* The next function is used only in Ocaml extraction...*) let pp_module mp = diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 0bd9efd255..a482cfc03d 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -55,6 +55,7 @@ val opened_libraries : unit -> ModPath.t list type kind = Term | Type | Cons | Mod val pp_global : kind -> GlobRef.t -> string +val pp_global_name : kind -> GlobRef.t -> string val pp_module : ModPath.t -> string val top_visible_mp : unit -> ModPath.t diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 088405da5d..6425c3111e 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -99,6 +99,8 @@ let str_global k r = let pp_global k r = str (str_global k r) +let pp_global_name k r = str (Common.pp_global k r) + let pp_modname mp = str (Common.pp_module mp) (* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *) @@ -451,7 +453,7 @@ let pp_val e typ = let pp_Dfix (rv,c,t) = let names = Array.map - (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + (fun r -> if is_inline_custom r then mt () else pp_global_name Term r) rv in let rec pp init i = if i >= Array.length rv then mt () @@ -504,7 +506,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (GlobRef.IndRef (kn,0)) in + let name = pp_global_name Type (GlobRef.IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -513,7 +515,7 @@ let pp_singleton kn packet = let pp_record kn fields ip_equiv packet = let ind = GlobRef.IndRef (kn,0) in - let name = pp_global Type ind in + let name = pp_global_name Type ind in let fieldnames = pp_fields ind fields in let l = List.combine fieldnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in @@ -535,7 +537,7 @@ let pp_ind co kn ind = let nextkwd = fnl () ++ str "and " in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else - pp_global Type (GlobRef.IndRef (kn,i))) + pp_global_name Type (GlobRef.IndRef (kn,i))) ind.ind_packets in let cnames = @@ -575,7 +577,7 @@ let pp_decl = function | Dterm (r,_,_) when is_inline_custom r -> mt () | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> - let name = pp_global Type r in + let name = pp_global_name Type r in let l = rename_tvars keywords l in let ids, def = try @@ -592,7 +594,7 @@ let pp_decl = function if is_custom r then str (" = " ^ find_custom r) else pp_function (empty_env ()) a in - let name = pp_global Term r in + let name = pp_global_name Term r in pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ()) | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) @@ -603,10 +605,10 @@ let pp_spec = function | Sind (kn,i) -> pp_mind kn i | Sval (r,t) -> let def = pp_type false [] t in - let name = pp_global Term r in + let name = pp_global_name Term r in hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def) | Stype (r,vl,ot) -> - let name = pp_global Type r in + let name = pp_global_name Type r in let l = rename_tvars keywords vl in let ids, def = try diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 3228c6afd4..2ca9a0e69d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -182,7 +182,7 @@ let catch_error_with_trace_loc loc use_finer call_trace f x = catching_error call_trace Exninfo.iraise e let catch_error_loc loc use_finer tac = - Proofview.tclOR tac (fun exn -> + Proofview.tclORELSE tac (fun exn -> let (e, info) = update_loc loc use_finer exn in Proofview.tclZERO ~info e) @@ -1084,7 +1084,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) -and eval_tactic ist tac : unit Proofview.tactic = match tac with +and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with | TacAtom {loc;v=t} -> let call = LtacAtomCall t in let trace = push_trace(loc,call) ist in @@ -1163,7 +1163,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) - | TacArg a -> interp_tactic ist (TacArg a) + | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v)) | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> @@ -1243,7 +1243,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let ist = { lfun = Id.Map.empty; poly; extra } in let appl = GlbAppl[r,[]] in Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false - (val_interp ~appl ist (Tacenv.interp_ltac r)) + (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r))) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1359,7 +1359,7 @@ and tactic_of_value ist vle = lfun = lfun; poly; extra = TacStore.set ist.extra f_trace []; } in - let tac = name_if_glob appl (eval_tactic ist t) in + let tac = name_if_glob appl (eval_tactic_ist ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) | VFun (appl,_,vmap,vars,_) -> let tactic_nm = @@ -1446,7 +1446,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = ; poly ; extra = TacStore.set ist.extra f_trace trace } in - let tac = eval_tactic ist t in + let tac = eval_tactic_ist ist t in let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy)) | _ -> Ftactic.return v @@ -1927,11 +1927,11 @@ let default_ist () = let eval_tactic t = Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *) Proofview.tclLIFT db_initialize <*> - interp_tactic (default_ist ()) t + eval_tactic_ist (default_ist ()) t let eval_tactic_ist ist t = Proofview.tclLIFT db_initialize <*> - interp_tactic ist t + eval_tactic_ist ist t (** FFI *) @@ -1977,7 +1977,7 @@ let interp_tac_gen lfun avoid_ids debug t = let extra = TacStore.set extra f_avoid_ids avoid_ids in let ist = { lfun; poly; extra } in let ltacvars = Id.Map.domain lfun in - interp_tactic ist + eval_tactic_ist ist (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end @@ -2094,7 +2094,7 @@ let () = register_interp0 wit_tactic interp let () = - let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in + let interp ist tac = eval_tactic_ist ist tac >>= fun () -> Ftactic.return () in register_interp0 wit_ltac interp let () = @@ -2121,7 +2121,7 @@ let _ = let eval lfun poly env sigma ty tac = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in - let tac = interp_tactic ist tac in + let tac = eval_tactic_ist ist tac in (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d7996a722a..d859fe51ab 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1047,7 +1047,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc = let uct = Evd.evar_universe_context (fst oc) in let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*> - Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc)) + Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc)) (fun _ -> Proofview.tclZERO dependent_apply_error) end diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index da623703a2..38b26d06b9 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -465,7 +465,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr = Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0 in let cvtac' = - Proofview.tclOR cvtac begin function + Proofview.tclORELSE cvtac begin function | (PRtype_error e, _) -> let error = Option.cata (fun (env, sigma, te) -> Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te)) diff --git a/tactics/equality.ml b/tactics/equality.ml index f1326a51a9..b4def7bb51 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1134,6 +1134,7 @@ let make_tuple env sigma (rterm,rty) lind = assert (not (noccurn sigma lind rty)); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in + let a = simpl env sigma a in let na = Context.Rel.Declaration.get_annot (lookup_rel lind env) in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb2e607012..70cea89ccb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1044,12 +1044,15 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = end end -let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) +let drop_intro_name (_ : Id.t) = Proofview.tclUNIT () + +let intro_gen n m f d = intro_then_gen n m f d drop_intro_name let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true false -let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false +let intro_using_then id = intro_then_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false +let intro_using id = intro_using_then id drop_intro_name let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false -let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false +let intro = intro_then drop_intro_name let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false @@ -1065,6 +1068,11 @@ let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l) +let rec intros_using_then_helper tac acc = function + | [] -> tac (List.rev acc) + | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l) +let intros_using_then l tac = intros_using_then_helper tac [] l + let intros = Tacticals.New.tclREPEAT intro let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5b397b15d0..00739306a7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -65,9 +65,11 @@ val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic +val intro_using_then : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic +val intros_using_then : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros_possibly_replacing : Id.t list -> unit Proofview.tactic diff --git a/test-suite/Makefile b/test-suite/Makefile index 6f49ae0d83..28add48b36 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -198,7 +198,6 @@ summary: $(call summary_dir, "Coqdoc tests", coqdoc); \ $(call summary_dir, "tools/ tests", tools); \ $(call summary_dir, "Unit tests", unit-tests); \ - $(call summary_dir, "Machine arithmetic tests", arithmetic); \ $(call summary_dir, "Ltac2 tests", ltac2); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ diff --git a/test-suite/bugs/closed/bug_12001.v b/test-suite/bugs/closed/bug_12001.v new file mode 100644 index 0000000000..19533e49f1 --- /dev/null +++ b/test-suite/bugs/closed/bug_12001.v @@ -0,0 +1,24 @@ +(* Argument names don't get mangled *) +Set Mangle Names. +Lemma leibniz_equiv_iff {A : Type} (x y : A) : True. +Proof. tauto. Qed. +Check leibniz_equiv_iff (A := nat) 2 3 : True. +Unset Mangle Names. + +(* Coq doesn't make up names for arguments *) +Definition bar (a a : nat) : nat := 3. +Arguments bar _ _ : assert. +Fail Arguments bar a a0 : assert. + +(* This definition caused an anomaly in a version of this PR +without the change to prepare_implicits *) +Set Implicit Arguments. +Definition foo (_ : nat) (_ : @eq nat ltac:(assumption) 2) : True := I. +Fail Check foo (H := 2). + +Definition baz (a b : nat) := b. +Arguments baz a {b}. +Set Mangle Names. +Definition baz2 (a b : nat) := b. +Arguments baz2 a {b}. +Unset Mangle Names. diff --git a/test-suite/bugs/closed/bug_12763.v b/test-suite/bugs/closed/bug_12763.v new file mode 100644 index 0000000000..6cbcc0d3b0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12763.v @@ -0,0 +1,6 @@ +Inductive bool_list := S (y : bool) (l : bool_list) | O. +Scheme Equality for bool_list. + +Set Mangle Names. +Scheme Equality for nat. +Scheme Equality for list. diff --git a/test-suite/bugs/closed/bug_12787.v b/test-suite/bugs/closed/bug_12787.v new file mode 100644 index 0000000000..2566e1f261 --- /dev/null +++ b/test-suite/bugs/closed/bug_12787.v @@ -0,0 +1,26 @@ +Inductive sigT3 {A: Type} {P: A -> Type} (Q: forall a: A, P a -> Type) := + existT3: forall a: A, forall b: P a, Q a b -> sigT3 Q +. + +Definition projT3_1 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) := + let 'existT3 _ x0 _ _ := a in x0. + +Definition projT3_2 {A: Type} {P: A -> Type} {Q: forall a: A, P a -> Type} (a: sigT3 Q) : P (projT3_1 a) := + let 'existT3 _ x0 x1 _ := a in x1. + + + +Lemma projT3_3_eq' (A B: Type) (Q: B -> Type) (a b: sigT3 (fun (_: A) b => Q b)) (H: a = b) : + unit. +Proof. + destruct a as [x0 x1 x2], b as [y0 y1 y2]. + assert (H' := f_equal projT3_1 H). + cbn in H'. + subst x0. + assert (H' := f_equal (projT3_2 (P := fun _ => B)) H). + cbn in H'. + subst x1. + + injection H as H'. + exact tt. +Qed. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e0aa758812..c28bb14eb3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -84,8 +84,6 @@ Argument lists should agree on the names they provide. The command has indeed failed with message: Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Some argument names are duplicated: F -The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6ac09cf771..6001850046 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,7 +48,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. -Fail Arguments eq_refl {F F}, [F] F : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/ErrorLocation_12774_3.out b/test-suite/output/ErrorLocation_12774_3.out new file mode 100644 index 0000000000..dbd3dbd1e2 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_12774_3.v b/test-suite/output/ErrorLocation_12774_3.v new file mode 100644 index 0000000000..c624402a81 --- /dev/null +++ b/test-suite/output/ErrorLocation_12774_3.v @@ -0,0 +1,4 @@ +Ltac f := auto; intro. +Goal False. +f. +Abort. diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out index 3e337e892d..2645524a70 100644 --- a/test-suite/output/Error_msg_diffs.out +++ b/test-suite/output/Error_msg_diffs.out @@ -1,4 +1,4 @@ -File "stdin", line 32, characters 0-12: +File "stdin", line 32, characters 0-11: [37;41;1mError:[0m In environment T : [33;1mType[0m diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index ef7667936c..2265028d3e 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x x0]%nat_scope +Arguments d2 [x x]%nat_scope map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/RecordMissingField.out b/test-suite/output/RecordMissingField.out index 7c80a6065f..28beee90b2 100644 --- a/test-suite/output/RecordMissingField.out +++ b/test-suite/output/RecordMissingField.out @@ -1,4 +1,16 @@ -File "stdin", line 8, characters 5-22: -Error: Cannot infer field y2p of record point2d in environment: -p : point2d - +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + 1; y2p := ?y2p |}) +More precisely: +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d +The command has indeed failed with message: +The following term contains unresolved implicit arguments: + (fun p : point2d => {| x2p := x2p p + (fun n : nat => ?n) 1; y2p := ?y2p |}) +More precisely: +- ?n: Cannot infer this placeholder of type "nat" in + environment: + p : point2d + n : nat +- ?y2p: Cannot infer field y2p of record point2d in environment: + p : point2d diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v index 84f1748fa0..8ca721564b 100644 --- a/test-suite/output/RecordMissingField.v +++ b/test-suite/output/RecordMissingField.v @@ -3,6 +3,10 @@ should contain missing field, and the inferred type of the record **) Record point2d := mkPoint { x2p: nat; y2p: nat }. - -Definition increment_x (p: point2d) : point2d := +Fail Definition increment_x (p: point2d) : point2d := {| x2p := x2p p + 1; |}. + +(* Here there is also an unresolved implicit, which should give an + understadable error as well *) +Fail Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + (fun n => _) 1; |}. diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.out b/test-suite/output/ssr_error_multiple_intro_after_case.out new file mode 100644 index 0000000000..51fb208ae9 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 0-11: +Error: x already used + diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v new file mode 100644 index 0000000000..1f87966693 --- /dev/null +++ b/test-suite/output/ssr_error_multiple_intro_after_case.v @@ -0,0 +1,3 @@ +Require Import ssreflect. +Goal forall p : nat * nat , True. +case => x x. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 563651cfa5..7acaa92b89 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -190,7 +190,7 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Arguments unit {m m0 α}. +Arguments unit {m _ α}. Arguments Monad : clear implicits. Notation "'return' t" := (unit t). diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index f47cdd8bf0..7a7e7d6e35 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -556,11 +556,17 @@ let list_id l = List.fold_left ( fun a decl -> let s' = Id.of_string (s'^"_lb")) ::a ) [] l + +let avoid_of_list_id list_id = + List.fold_left (fun avoid (s,seq,sbl,slb) -> + List.fold_left (fun avoid id -> Id.Set.add id avoid) + avoid [s;seq;sbl;slb]) + Id.Set.empty list_id + (* build the right eq_I A B.. N eq_A .. eq_N *) -let eqI ind l = - let list_id = list_id l in +let eqI ind list_id = let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@ (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) and e = match lookup_scheme beq_scheme_kind ind with @@ -568,7 +574,7 @@ let eqI ind l = | None -> user_err ~hdr:"AutoIndDecl.eqI" (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed."); - in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)) + in mkApp(e,eA) (**********************************************************************) (* Boolean->Leibniz *) @@ -576,12 +582,12 @@ let eqI ind l = open Namegen let compute_bl_goal ind lnamesparrec nparrec = - let eqI = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in + let eqI = eqI ind list_id in + let avoid = avoid_of_list_id list_id in + let x = next_ident_away (Id.of_string "x") avoid in + let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in let create_input c = - let x = next_ident_away (Id.of_string "x") avoid and - y = next_ident_away (Id.of_string "y") avoid in let bl_typ = List.map (fun (s,seq,_,_) -> mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) ( mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) ( @@ -607,88 +613,74 @@ let compute_bl_goal ind lnamesparrec nparrec = in mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec in - let n = next_ident_away (Id.of_string "x") avoid and - m = next_ident_away (Id.of_string "y") avoid in let u = Univ.Instance.empty in create_input ( - mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( - mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( + mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( + mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( mkArrow - (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|])) + (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar x;mkVar y|]);tt ()|])) Sorts.Relevant - (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) + (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar x;mkVar y|])) ))) let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in - let avoid = ref [] in - let first_intros = - ( List.map (fun (s,_,_,_) -> s ) list_id ) @ - ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @ - ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) - in - let fresh_id s gl = - let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in - avoid := fresh::(!avoid); fresh - in - Proofview.Goal.enter begin fun gl -> - let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in - let freshn = fresh_id (Id.of_string "x") gl in - let freshm = fresh_id (Id.of_string "y") gl in - let freshz = fresh_id (Id.of_string "Z") gl in - (* try with *) - Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; - intro_using freshn ; - induct_on (EConstr.mkVar freshn); - intro_using freshm; - destruct_on (EConstr.mkVar freshm); - intro_using freshz; - intros; - Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity my_discr_tac - ); - simpl_in_hyp (freshz,Locus.InHyp); -(* + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) + @ ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) + @ ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) + in + intros_using_then first_intros begin fun fresh_first_intros -> + Tacticals.New.tclTHENLIST [ + intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn)); + intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm)); + intro_using_then (Id.of_string "Z") begin fun freshz -> + Tacticals.New.tclTHENLIST [ + intros; + Tacticals.New.tclTRY ( + Tacticals.New.tclORELSE reflexivity my_discr_tac + ); + simpl_in_hyp (freshz,Locus.InHyp); + (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). -*) - Tacticals.New.tclREPEAT ( - Tacticals.New.tclTHENLIST [ - Simple.apply_in freshz (EConstr.of_constr (andb_prop())); - Proofview.Goal.enter begin fun gl -> - let fresht = fresh_id (Id.of_string "Z") gl in - destruct_on_as (EConstr.mkVar freshz) - (IntroOrPattern [[CAst.make @@ IntroNaming (IntroIdentifier fresht); - CAst.make @@ IntroNaming (IntroIdentifier freshz)]]) - end - ]); -(* + *) + Tacticals.New.tclREPEAT ( + Tacticals.New.tclTHENLIST [ + Simple.apply_in freshz (EConstr.of_constr (andb_prop())); + destruct_on_as (EConstr.mkVar freshz) + (IntroOrPattern [[CAst.make @@ IntroNaming (IntroFresh (Id.of_string "Z")); + CAst.make @@ IntroNaming (IntroIdentifier freshz)]]) + ]); + (* Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto -*) - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let sigma = Tacmach.New.project gl in - match EConstr.kind sigma concl with - | App (c,ca) -> ( - match EConstr.kind sigma c with - | Ind (indeq, u) -> - if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type") - then - Tacticals.New.tclTHEN - (do_replace_bl bl_scheme_key ind - (!avoid) - nparrec (ca.(2)) - (ca.(1))) - Auto.default_auto - else - Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") - ) - | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - end + *) + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in + match EConstr.kind sigma concl with + | App (c,ca) -> ( + match EConstr.kind sigma c with + | Ind (indeq, u) -> + if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type") + then + Tacticals.New.tclTHEN + (do_replace_bl bl_scheme_key ind + (List.rev fresh_first_intros) + nparrec (ca.(2)) + (ca.(1))) + Auto.default_auto + else + Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") + ) + | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + end - ] - end + ] + end + ] + end let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -729,11 +721,11 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eq = eq () and tt = tt () and bb = bb () in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in - let eqI = eqI ind lnamesparrec in + let avoid = avoid_of_list_id list_id in + let eqI = eqI ind list_id in + let x = next_ident_away (Id.of_string "x") avoid in + let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in let create_input c = - let x = next_ident_away (Id.of_string "x") avoid and - y = next_ident_away (Id.of_string "y") avoid in let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) ( mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) ( @@ -760,73 +752,62 @@ let compute_lb_goal ind lnamesparrec nparrec = in mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec in - let n = next_ident_away (Id.of_string "x") avoid and - m = next_ident_away (Id.of_string "y") avoid in let u = Univ.Instance.empty in create_input ( - mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( - mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( + mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) ( + mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) ( mkArrow - (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|])) + (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar x;mkVar y|])) Sorts.Relevant - (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) + (mkApp(eq,[|bb;mkApp(eqI,[|mkVar x;mkVar y|]);tt|])) ))) let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in - let avoid = ref [] in - let first_intros = - ( List.map (fun (s,_,_,_) -> s ) list_id ) @ - ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ - ( List.map (fun (_,_,_,slb) -> slb) list_id ) - in - let fresh_id s gl = - let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in - avoid := fresh::(!avoid); fresh - in - Proofview.Goal.enter begin fun gl -> - let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in - let freshn = fresh_id (Id.of_string "x") gl in - let freshm = fresh_id (Id.of_string "y") gl in - let freshz = fresh_id (Id.of_string "Z") gl in - (* try with *) - Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; - intro_using freshn ; - induct_on (EConstr.mkVar freshn); - intro_using freshm; - destruct_on (EConstr.mkVar freshm); - intro_using freshz; - intros; - Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity my_discr_tac - ); - my_inj_tac freshz; - intros; simpl_in_concl; - Auto.default_auto; - Tacticals.New.tclREPEAT ( - Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro())); - simplest_split ;Auto.default_auto ] - ); - Proofview.Goal.enter begin fun gls -> - let concl = Proofview.Goal.concl gls in - let sigma = Tacmach.New.project gl in - (* assume the goal to be eq (eq_type ...) = true *) - match EConstr.kind sigma concl with - | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with - | App(c',ca') -> - let n = Array.length ca' in - do_replace_lb mode lb_scheme_key - (!avoid) - nparrec - ca'.(n-2) ca'.(n-1) - | _ -> - Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - ) - | _ -> - Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - end - ] - end + let first_intros = + ( List.map (fun (s,_,_,_) -> s ) list_id ) + @ ( List.map (fun (_,seq,_,_) -> seq) list_id ) + @ ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in + intros_using_then first_intros begin fun fresh_first_intros -> + Tacticals.New.tclTHENLIST [ + intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn)); + intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm)); + intro_using_then (Id.of_string "Z") begin fun freshz -> + Tacticals.New.tclTHENLIST [ + intros; + Tacticals.New.tclTRY ( + Tacticals.New.tclORELSE reflexivity my_discr_tac + ); + my_inj_tac freshz; + intros; simpl_in_concl; + Auto.default_auto; + Tacticals.New.tclREPEAT ( + Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro())); + simplest_split ;Auto.default_auto ] + ); + Proofview.Goal.enter begin fun gls -> + let concl = Proofview.Goal.concl gls in + let sigma = Tacmach.New.project gls in + (* assume the goal to be eq (eq_type ...) = true *) + match EConstr.kind sigma concl with + | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with + | App(c',ca') -> + let n = Array.length ca' in + do_replace_lb mode lb_scheme_key + (List.rev fresh_first_intros) + nparrec + ca'.(n-2) ca'.(n-1) + | _ -> + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") + ) + | _ -> + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") + end + ] + end + ] + end let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") @@ -868,10 +849,10 @@ let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); let eq = eq () and tt = tt () and bb = bb () in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in + let avoid = avoid_of_list_id list_id in + let x = next_ident_away (Id.of_string "x") avoid in + let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in let create_input c = - let x = next_ident_away (Id.of_string "x") avoid and - y = next_ident_away (Id.of_string "y") avoid in let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) ( mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) ( @@ -912,12 +893,10 @@ let compute_dec_goal ind lnamesparrec nparrec = in mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec in - let n = next_ident_away (Id.of_string "x") avoid and - m = next_ident_away (Id.of_string "y") avoid in - let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in + let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar x;mkVar y|]) in create_input ( - mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd ind (2*nparrec)) ( - mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) ( + mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd ind (2*nparrec)) ( + mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) ( mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) ) ) @@ -925,83 +904,89 @@ let compute_dec_goal ind lnamesparrec nparrec = let compute_dec_tact ind lnamesparrec nparrec = let eq = eq () and tt = tt () - and ff = ff () and bb = bb () in + and ff = ff () and bb = bb () in let list_id = list_id lnamesparrec in find_scheme beq_scheme_kind ind >>= fun _ -> - let eqI = eqI ind lnamesparrec in - let avoid = ref [] in + let _non_fresh_eqI = eqI ind list_id in let eqtrue x = mkApp(eq,[|bb;x;tt|]) in let eqfalse x = mkApp(eq,[|bb;x;ff|]) in let first_intros = - ( List.map (fun (s,_,_,_) -> s ) list_id ) @ - ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ - ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @ - ( List.map (fun (_,_,_,slb) -> slb) list_id ) - in - let fresh_id s gl = - let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in - avoid := fresh::(!avoid); fresh + ( List.map (fun (s,_,_,_) -> s ) list_id ) + @ ( List.map (fun (_,seq,_,_) -> seq) list_id ) + @ ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) + @ ( List.map (fun (_,_,_,slb) -> slb) list_id ) in - Proofview.Goal.enter begin fun gl -> - let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in - let freshn = fresh_id (Id.of_string "x") gl in - let freshm = fresh_id (Id.of_string "y") gl in - let freshH = fresh_id (Id.of_string "H") gl in - let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in - let arfresh = Array.of_list fresh_first_intros in - let xargs = Array.sub arfresh 0 (2*nparrec) in - find_scheme bl_scheme_kind ind >>= fun c -> - let blI = mkConst c in - find_scheme lb_scheme_kind ind >>= fun c -> - let lbI = mkConst c in - Tacticals.New.tclTHENLIST [ - intros_using fresh_first_intros; - intros_using [freshn;freshm]; - (*we do this so we don't have to prove the same goal twice *) - assert_by (Name freshH) (EConstr.of_constr ( - mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) - )) - (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto); - + let fresh_id s gl = fresh_id_in_env (Id.Set.empty) s (Proofview.Goal.env gl) in + intros_using_then first_intros begin fun fresh_first_intros -> + let eqI = + let a = Array.of_list fresh_first_intros in + let n = List.length list_id in + assert (Int.equal (Array.length a) (4 * n)); + let fresh_list_id = + List.init n (fun i -> (Array.get a i, Array.get a (i+n), + Array.get a (i+2*n), Array.get a (i+3*n))) in + eqI ind fresh_list_id + in + intro_using_then (Id.of_string "x") begin fun freshn -> + intro_using_then (Id.of_string "y") begin fun freshm -> Proofview.Goal.enter begin fun gl -> - let freshH2 = fresh_id (Id.of_string "H") gl in - Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [ - (* left *) - Tacticals.New.tclTHENLIST [ - simplest_left; - apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs))); - Auto.default_auto - ] - ; - - (*right *) - Proofview.Goal.enter begin fun gl -> - let freshH3 = fresh_id (Id.of_string "H") gl in - Tacticals.New.tclTHENLIST [ - simplest_right ; - unfold_constr (Coqlib.lib_ref "core.not.type"); - intro; - Equality.subst_all (); - assert_by (Name freshH3) - (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))) - (Tacticals.New.tclTHENLIST [ - apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs))); - Auto.default_auto - ]); - Equality.general_rewrite_bindings_in true - Locus.AllOccurrences true false - (List.hd !avoid) - ((EConstr.mkVar (List.hd (List.tl !avoid))), - NoBindings - ) - true; - my_discr_tac + let freshH = fresh_id (Id.of_string "H") gl in + let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in + let arfresh = Array.of_list fresh_first_intros in + let xargs = Array.sub arfresh 0 (2*nparrec) in + find_scheme bl_scheme_kind ind >>= fun c -> + let blI = mkConst c in + find_scheme lb_scheme_kind ind >>= fun c -> + let lbI = mkConst c in + Tacticals.New.tclTHENLIST [ + (*we do this so we don't have to prove the same goal twice *) + assert_by (Name freshH) (EConstr.of_constr ( + mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) + )) + (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto); + + Proofview.Goal.enter begin fun gl -> + let freshH2 = fresh_id (Id.of_string "H") gl in + Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [ + (* left *) + Tacticals.New.tclTHENLIST [ + simplest_left; + apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs))); + Auto.default_auto + ] + ; + + (*right *) + Proofview.Goal.enter begin fun gl -> + let freshH3 = fresh_id (Id.of_string "H") gl in + Tacticals.New.tclTHENLIST [ + simplest_right ; + unfold_constr (Coqlib.lib_ref "core.not.type"); + intro; + Equality.subst_all (); + assert_by (Name freshH3) + (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))) + (Tacticals.New.tclTHENLIST [ + apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs))); + Auto.default_auto + ]); + Equality.general_rewrite_bindings_in true + Locus.AllOccurrences true false + freshH3 + ((EConstr.mkVar freshH2), + NoBindings + ) + true; + my_discr_tac + ] + end + ] + end ] - end - ] + end end - ] - end + end + end let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 360e228bfc..be9cc059a7 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -213,14 +213,6 @@ let vernac_arguments ~section_local reference args more_implicits flags = in CErrors.user_err ~hdr:"vernac_declare_arguments" msg end; - let duplicate_names = - List.duplicates Name.equal (List.filter ((!=) Anonymous) names) - in - if not (List.is_empty duplicate_names) then begin - CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++ - prlist_with_sep pr_comma Name.print duplicate_names) - end; - let implicits = List.map (fun { name; implicit_status = i } -> (name,i)) args in diff --git a/vernac/declare.ml b/vernac/declare.ml index eedbee852b..66537c2978 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -642,14 +642,32 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = dref (* Preparing proof entries *) +let error_unresolved_evars env sigma t evars = + let pr_unresolved_evar e = + hov 2 (str"- " ++ Printer.pr_existential_key sigma e ++ str ": " ++ + Himsg.explain_pretype_error env sigma + (Pretype_errors.UnsolvableImplicit (e,None))) + in + CErrors.user_err (hov 0 begin + str "The following term contains unresolved implicit arguments:"++ fnl () ++ + str " " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++ + str "More precisely: " ++ fnl () ++ + v 0 (prlist_with_sep cut pr_unresolved_evar (Evar.Set.elements evars)) + end) + +let check_evars_are_solved env sigma t = + let t = EConstr.of_constr t in + let evars = Evarutil.undefined_evars_of_term sigma t in + if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars let prepare_definition ~info ~opaque ~body ~typ sigma = let { Info.poly; udecl; inline; _ } = info in let env = Global.env () in - Pretyping.check_evars_are_solved ~program_mode:false env sigma; - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false sigma (fun nf -> nf body, Option.map nf typ) in + Option.iter (check_evars_are_solved env sigma) types; + check_evars_are_solved env sigma body; let univs = Evd.check_univ_decl ~poly sigma udecl in let entry = definition_entry ~opaque ~inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in diff --git a/vernac/declare.mli b/vernac/declare.mli index c5a8afbad5..3001d0d206 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -117,8 +117,7 @@ end normalized w.r.t. the passed [evar_map] [sigma]. Universes should be handled properly, including minimization and restriction. Note that [sigma] is checked for unresolved evars, thus you should be - careful not to submit open terms or evar maps with stale, - unresolved existentials *) + careful not to submit open terms *) val declare_definition : info:Info.t -> cinfo:EConstr.t option CInfo.t |