Leonardo de Moura 11fbee269b fix(frontends/lean/parser): must save state of name_generator in parser snapshot ... To provide typing and auto-completion information, we create a background process by starting lean with the option --server. In "server" mode, we create snapshots of the parser state. The idea is to be able to quickly reprocess a file when the user makes a modification. This commit fixes a bug in the snapshot operation. It was not saving in the snapshots the unique name generator used by the parser. By creating a fresh name generator, we may accidentally assign the same internal name to two different constants. This bug triggered the crash described in issue #593. This commit fixes the test in the comment https://github.com/leanprover/lean/issues/593#issuecomment-101768484 This commit also adds a smaller version of the problem to the test suite		2015-05-13 12:28:23 -07:00
..
alias.input
alias.input.expected.out	feat(library/tactic): add 'let' tactic	2015-04-28 17:24:43 -07:00
apply_info.input
apply_info.input.expected.out
auto_comp.input	feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations	2015-02-25 17:00:10 -08:00
auto_comp.input.expected.out	feat(frontends/lean): new semantics for "protected" declarations	2015-02-11 14:09:25 -08:00
class_bug.lean
coe.input
coe.input.expected.out
coe.lean
commands.input	fix(tests/lean/interactive): do not compare output of trace using non-deterministic commands such as "WAIT ms"	2015-01-30 09:52:42 -08:00
commands.input.expected.out	fix(tests/lean/interactive): do not compare output of trace using non-deterministic commands such as "WAIT ms"	2015-01-30 09:52:42 -08:00
commands.trace	fix(tests/lean/interactive): do not compare output of trace using non-deterministic commands such as "WAIT ms"	2015-01-30 09:52:42 -08:00
consume_args.input
consume_args.input.expected.out
eq2.input	feat(frontends/lean): new semantics for "protected" declarations	2015-02-11 14:09:25 -08:00
eq2.input.expected.out
eq2.lean	refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'	2015-05-02 15:15:35 -07:00
extra_type.input	feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations	2015-02-25 17:00:10 -08:00
extra_type.input.expected.out	feat(frontends/lean): new semantics for "protected" declarations	2015-02-11 14:09:25 -08:00
findp.input
findp.input.expected.out	fix(tests/lean/interactive/findp): adjust test output	2015-04-30 15:45:15 -07:00
findp.lean
in1.input
in1.input.expected.out
in2.input	fix(tests/lean/interactive): adjust tests to reflect changes in the standard library	2015-03-04 18:30:31 -08:00
in2.input.expected.out	fix(tests/lean/interactive): adjust tests to reflect changes in the standard library	2015-03-04 18:30:31 -08:00
in4.input
in4.input.expected.out
in5.input
in5.input.expected.out
info.input
info.input.expected.out
missing.input
missing.input.expected.out
missing.lean	feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations	2015-02-25 17:00:10 -08:00
mod.input
mod.input.expected.out
notation_info.input
notation_info.input.expected.out
num2.input
num2.input.expected.out	feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed	2015-03-13 14:47:21 -07:00
num2.lean	feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations	2015-02-25 17:00:10 -08:00
options_cmd.trace
optstack.input
optstack.input.expected.out
overload_coercion.input	test(tests/lean/interactive): add tests for coercion and overload info	2015-01-29 16:39:27 -08:00
overload_coercion.input.expected.out	test(tests/lean/interactive): add tests for coercion and overload info	2015-01-29 16:39:27 -08:00
proof_qed.input
proof_qed.input.expected.out
proof_qed.lean
proof_state_info.input	feat(frontends/lean): uniform notation for lists in tactics	2015-03-27 17:54:48 -07:00
proof_state_info.input.expected.out
proof_state_info2.input	feat(frontends/lean): uniform notation for lists in tactics	2015-03-27 17:54:48 -07:00
proof_state_info2.input.expected.out
proof_state_info3.input	feat(frontends/lean): uniform notation for lists in tactics	2015-03-27 17:54:48 -07:00
proof_state_info3.input.expected.out	feat(frontends/lean): uniform notation for lists in tactics	2015-03-27 17:54:48 -07:00
sec_info_bug.input	chore(tests/lean/interactive/sec_info_bug): remove 'context' command from test	2015-04-21 19:52:01 -07:00
sec_info_bug.input.expected.out
simple.lean
simple3.lean
snapshot_bug.input	fix(frontends/lean/parser): must save state of name_generator in parser snapshot	2015-05-13 12:28:23 -07:00
snapshot_bug.input.expected.out	fix(frontends/lean/parser): must save state of name_generator in parser snapshot	2015-05-13 12:28:23 -07:00
snapshot_bug.lean	fix(frontends/lean/parser): must save state of name_generator in parser snapshot	2015-05-13 12:28:23 -07:00
sorry2.lean
sync.input
sync.input.expected.out
t4.input
t4.input.expected.out
test_single.sh	fix(test*.sh): allow spaces in filename	2015-03-28 23:29:52 -04:00
var.input
var.input.expected.out
whnfinst.lean	feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible	2015-02-24 16:12:35 -08:00