test-suite/misc · coq · Tangled

forked from coq/coq

coq test-suite misc

22 folders · 53 files

Gaëtan Gilbert · Slightly more standard test files · 3w ago

Add the test as a misc script.

assumptions-norec

Slightly more standard test files

Test case for attributes on hooks

timelog2html visuals for heap usage

Use Corelib instead of Stdlib as namespace for rocq-core

Cleanup beautify handling

coqdep-require-filter-categories

rocqdep print location for module not found warning

coqdep-string-literals

Skip string literals when rocq dep looks for the end of a sentence

Update various URLs after the renaming

try to improve deps-order-distinct-root test

Adding tests for testing exit status and #use"include".

rocqdep print location for module not found warning

extraction-external-language

Extraction: use a CString.Map for languages, diff test output

non-marshalable-state

Abstract away the Summary reference type.

norec-validation-order

checker: validate every library named on the command line

poly-capture-global-univs

Monomorphic Declare entries now use Univ.ContextSet.t.

print-assumptions-vok

Adding a test for #13589.

Add test for #14475

quotation_token

rename package coq-core -> rocq-runtime

side-eff-leak-univs

Add support for parsing elimination constraints

tc_declaration_observer

Pass mode to class observer

[build] Use dune to build OCaml code.

Library: fix library_is_loaded always returning true

Add a testcase.

Add the test as a misc script.

[toplevel] Deprecate the `-compile` flag in favor of `coqc`.

Fixing #7393: ignore dots in comments parsed by coqdep.

[toplevel] Deprecate the `-compile` flag in favor of `coqc`.

assumptions-norec.sh

checker: record sealed assumptions in admitted libraries

Test case for attributes on hooks

Remove dependency on BinNat.

[toplevel] Deprecate the `-compile` flag in favor of `coqc`.

bench-render.sh

skip trailing cr in some tests

[coqc] Check that no obligations remain before saving a .vo

Fixing #7393: ignore dots in comments parsed by coqdep.

changelog test use configure.ml instead of generated file

comment-lexing.sh

skip trailing cr in some tests

coq_environment.sh

fix coq_environment test bad cp

coq_makefile_destination_of.sh

fix quoting in destinaton_of test

coqc_dash_vok: add shell-script test

coqc_dash_vok: add shell-script test

coqdep-require-filter-categories.sh

rocqdep print location for module not found warning

coqdep-string-literals.sh

Fix coqdep-string-literals test on macOS

coqdoc-options.sh

test suite use rocq instead of coqc etc

deps-checksum.sh

Don't rely on ambiguous loading for deps-checksum test

deps-order-distinct-root.sh

Test suite avoid using rcfile

deps-order-from.sh

rename coqworker -> rocqworker

deps-order-subdir1-file.sh

rename coqworker -> rocqworker

deps-order-subdir2-file.sh

rename coqworker -> rocqworker

deps-order-subdir3-file.sh

rename coqworker -> rocqworker

Stricter non-ambiguousness check in Require

test-suite: stop using `mktemp /tmp/foo`

[toplevel] Split interactive toplevel and compiler binaries.

external-deps.sh

rename coqworker -> rocqworker

extraction-external-language.sh

Extraction: use a CString.Map for languages, diff test output

load-succeed.sh

Test suite avoid using rcfile

locate-library.sh

Library: fix library_is_loaded always returning true

non-marshalable-state.sh

Test suite avoid using rcfile

norec-validation-order.sh

checker: validate every library named on the command line

poly-capture-global-univs.sh

test suite use rocq instead of coqc etc

print-assumptions-vok.sh

Test suite avoid using rcfile

print-mod-uid.sh

Move print-mod-uid to main rocq exe instead of rocq repl

Rename "Welcome to Coq" -> "Welcome to Rocq"

Test suite avoid using rcfile

quotation_token.sh

test suite use rocq instead of coqc etc

redirect_printing.out

[topfmt] Set formatter + flush fix

redirect_printing.sh

[topfmt] Set formatter + flush fix

redirect_printing.v

[topfmt] Set formatter + flush fix

Add [rocq find] test.

rocqchk_vm_bytecode.sh

Do not trust the serialized VM bytecode in rocqchk

side-eff-leak-univs.sh

test suite use rocq instead of coqc etc

silence_deprecated_env_var.sh

Apply warning flags before computing load paths (#20743)

tc_declaration_observer.sh

skip trailing cr in some tests

[test-suite] Fix misc test after removing stdlib

Adding a test for votour.