Edwin Brady c88bf7af8d Fix import loading ... This was taking too long, and adding too many things, because it was going too deep in the name of having everything accessible at the REPL and for the compiler. So, it's done a bit differently now, only chasing everything on a "full" load (i.e., final load at the REPL) This has some effects: + As systems get bigger, load time gets better (on my machine, checking Idris.Main now takes 52s from scratch, down from 76s) + You might find import errors that you didn't previously get, because things were being imported that shouldn't have been. The new way is correct! An unfortunate effect is that sometimes you end up getting "undefined name" errors even if you didn't explicitly use the name, because sometimes a module uses a name from another module in a type, which then gets exported, and eventually needs to be reduced. This mostly happens because there is a compile time check that should be done which I haven't implemented yet. That is, public export definitions should only be allowed to use names that are also public export. I'll get to this soon.		2020-05-27 15:49:03 +01:00
..
basic001	Add test script	2020-05-19 18:25:18 +01:00
basic002	Add test script	2020-05-19 18:25:18 +01:00
basic003	Add test script	2020-05-19 18:25:18 +01:00
basic004	Add test script	2020-05-19 18:25:18 +01:00
basic005	Add test script	2020-05-19 18:25:18 +01:00
basic006	Add test script	2020-05-19 18:25:18 +01:00
basic007	Add test script	2020-05-19 18:25:18 +01:00
basic008	Add test script	2020-05-19 18:25:18 +01:00
basic009	Add test script	2020-05-19 18:25:18 +01:00
basic010	Add test script	2020-05-19 18:25:18 +01:00
basic011	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
basic012	Add test script	2020-05-19 18:25:18 +01:00
basic013	Add test script	2020-05-19 18:25:18 +01:00
basic014	Add test script	2020-05-19 18:25:18 +01:00
basic015	Add test script	2020-05-19 18:25:18 +01:00
basic016	Add test script	2020-05-19 18:25:18 +01:00
basic017	Add test script	2020-05-19 18:25:18 +01:00
basic018	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
basic019	Allow _ for names in pi binders	2020-05-25 13:14:51 +01:00
basic020	Add test script	2020-05-19 18:25:18 +01:00
basic021	Add test script	2020-05-19 18:25:18 +01:00
basic022	Add test script	2020-05-19 18:25:18 +01:00
basic023	Add test script	2020-05-19 18:25:18 +01:00
basic024	Add test script	2020-05-19 18:25:18 +01:00
basic025	Add test script	2020-05-19 18:25:18 +01:00
basic026	Add test script	2020-05-19 18:25:18 +01:00
basic027	Add test script	2020-05-19 18:25:18 +01:00
basic028	Add test script	2020-05-19 18:25:18 +01:00
basic029	Add test script	2020-05-19 18:25:18 +01:00
basic030	Allow _ for names in pi binders	2020-05-25 13:14:51 +01:00
basic031	Add test script	2020-05-19 18:25:18 +01:00
basic032	Add test script	2020-05-19 18:25:18 +01:00
basic033	Add test script	2020-05-19 18:25:18 +01:00
basic034	Add test script	2020-05-19 18:25:18 +01:00
basic035	Fix build	2020-05-25 16:45:33 +01:00
basic036	Allow _ for names in pi binders	2020-05-25 13:14:51 +01:00
basic037	Add test script	2020-05-19 18:25:18 +01:00
basic038	Add test script	2020-05-19 18:25:18 +01:00
basic039	Add AllGuarded flag for functions	2020-05-22 17:27:18 +01:00
basic040	Add test script	2020-05-19 18:25:18 +01:00
coverage001	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
coverage002	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
coverage003	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
coverage004	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
coverage005	Fix import loading	2020-05-27 15:49:03 +01:00
coverage006	Better checking for empty types	2020-05-23 11:03:54 +01:00
coverage007	[ typo ] in test coverage007	2020-05-23 13:38:33 +01:00
coverage008	update golden files	2020-05-25 10:06:52 -07:00
coverage009	Warn on detecting unreachable patterns	2020-05-25 00:16:49 +01:00
error001	Add test script	2020-05-19 18:25:18 +01:00
error002	Add test script	2020-05-19 18:25:18 +01:00
error003	Add test script	2020-05-19 18:25:18 +01:00
error004	Add test script	2020-05-19 18:25:18 +01:00
error005	Add test script	2020-05-19 18:25:18 +01:00
error006	Add test script	2020-05-19 18:25:18 +01:00
error007	Add test script	2020-05-19 18:25:18 +01:00
error008	Add test script	2020-05-19 18:25:18 +01:00
error009	Add test script	2020-05-19 18:25:18 +01:00
error010	Add test script	2020-05-19 18:25:18 +01:00
import001	Add test script	2020-05-19 18:25:18 +01:00
import002	Fix import loading	2020-05-27 15:49:03 +01:00
import003	Add test script	2020-05-19 18:25:18 +01:00
import004	Add test script	2020-05-19 18:25:18 +01:00
interactive001	Add test script	2020-05-19 18:25:18 +01:00
interactive002	Add test script	2020-05-19 18:25:18 +01:00
interactive003	Add test script	2020-05-19 18:25:18 +01:00
interactive004	Add test script	2020-05-19 18:25:18 +01:00
interactive005	Add test script	2020-05-19 18:25:18 +01:00
interactive006	Add test script	2020-05-19 18:25:18 +01:00
interactive007	Add test script	2020-05-19 18:25:18 +01:00
interactive008	Add test script	2020-05-19 18:25:18 +01:00
interactive009	Add test script	2020-05-19 18:25:18 +01:00
interactive010	Add test script	2020-05-19 18:25:18 +01:00
interactive011	Add test script	2020-05-19 18:25:18 +01:00
interactive012	Add test script	2020-05-19 18:25:18 +01:00
interactive013	[ fix ] preserve spacing during update	2020-05-23 14:41:44 +01:00
interface001	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
interface002	Add test script	2020-05-19 18:25:18 +01:00
interface003	Add test script	2020-05-19 18:25:18 +01:00
interface004	Add test script	2020-05-19 18:25:18 +01:00
interface005	Add test script	2020-05-19 18:25:18 +01:00
interface006	Add test script	2020-05-19 18:25:18 +01:00
interface007	Add test script	2020-05-19 18:25:18 +01:00
interface008	Add test script	2020-05-19 18:25:18 +01:00
interface009	Add test script	2020-05-19 18:25:18 +01:00
interface010	Add test script	2020-05-19 18:25:18 +01:00
interface011	Add test script	2020-05-19 18:25:18 +01:00
interface012	Add test script	2020-05-19 18:25:18 +01:00
interface013	Add test script	2020-05-19 18:25:18 +01:00
interface014	Add test script	2020-05-19 18:25:18 +01:00
interface015	Add test script	2020-05-19 18:25:18 +01:00
interpreter001	Add test script	2020-05-19 18:25:18 +01:00
lazy001	Add test script	2020-05-19 18:25:18 +01:00
linear001	Add test script	2020-05-19 18:25:18 +01:00
linear002	Add test script	2020-05-19 18:25:18 +01:00
linear003	Add test script	2020-05-19 18:25:18 +01:00
linear004	Allow _ for names in pi binders	2020-05-25 13:14:51 +01:00
linear005	Add test script	2020-05-19 18:25:18 +01:00
linear006	Add test script	2020-05-19 18:25:18 +01:00
linear007	Add test script	2020-05-19 18:25:18 +01:00
linear008	Add test script	2020-05-19 18:25:18 +01:00
linear009	Allow _ for names in pi binders	2020-05-25 13:14:51 +01:00
literate001	Add test script	2020-05-19 18:25:18 +01:00
literate002	Add test script	2020-05-19 18:25:18 +01:00
literate003	Add test script	2020-05-19 18:25:18 +01:00
literate004	Add test script	2020-05-19 18:25:18 +01:00
literate005	Add test script	2020-05-19 18:25:18 +01:00
literate006	Add test script	2020-05-19 18:25:18 +01:00
literate007	Add test script	2020-05-19 18:25:18 +01:00
literate008	Add test script	2020-05-19 18:25:18 +01:00
literate009	Add test script	2020-05-19 18:25:18 +01:00
literate010	Add test script	2020-05-19 18:25:18 +01:00
literate011	Add test script	2020-05-19 18:25:18 +01:00
literate012	Add test script	2020-05-19 18:25:18 +01:00
params001	Add test script	2020-05-19 18:25:18 +01:00
perf001	Add test script	2020-05-19 18:25:18 +01:00
perf002	Add test script	2020-05-19 18:25:18 +01:00
perf003	Add test script	2020-05-19 18:25:18 +01:00
perf004	Add test script	2020-05-19 18:25:18 +01:00
perror001	Add test script	2020-05-19 18:25:18 +01:00
perror002	Add test script	2020-05-19 18:25:18 +01:00
perror003	Add test script	2020-05-19 18:25:18 +01:00
perror004	Add test script	2020-05-19 18:25:18 +01:00
perror005	Add test script	2020-05-19 18:25:18 +01:00
perror006	Add test script	2020-05-19 18:25:18 +01:00
pkg001	Add test script	2020-05-19 18:25:18 +01:00
pkg002	Add test script	2020-05-19 18:25:18 +01:00
pkg003	Allow cli given option overriding for ipkg cmds.	2020-05-26 14:41:09 +01:00
real001	Add test script	2020-05-19 18:25:18 +01:00
real002	Add test script	2020-05-19 18:25:18 +01:00
record001	Add test script	2020-05-19 18:25:18 +01:00
record002	Add test script	2020-05-19 18:25:18 +01:00
record003	Add test script	2020-05-19 18:25:18 +01:00
record004	Finish tests	2020-05-19 20:06:37 +01:00
reg001	Add test script	2020-05-19 18:25:18 +01:00
reg002	Add test script	2020-05-19 18:25:18 +01:00
reg003	Fix import loading	2020-05-27 15:49:03 +01:00
reg004	Add test script	2020-05-19 18:25:18 +01:00
reg005	Add test script	2020-05-19 18:25:18 +01:00
reg006	Add test script	2020-05-19 18:25:18 +01:00
reg007	Add test script	2020-05-19 18:25:18 +01:00
reg008	Add test script	2020-05-19 18:25:18 +01:00
reg009	Add test script	2020-05-19 18:25:18 +01:00
reg010	Add test script	2020-05-19 18:25:18 +01:00
reg011	Add test script	2020-05-19 18:25:18 +01:00
reg012	Add test script	2020-05-19 18:25:18 +01:00
reg013	Add test script	2020-05-19 18:25:18 +01:00
reg014	Add test script	2020-05-19 18:25:18 +01:00
reg015	Add test script	2020-05-19 18:25:18 +01:00
reg016	Add test script	2020-05-19 18:25:18 +01:00
reg017	Allow _ for names in pi binders	2020-05-25 13:14:51 +01:00
reg018	Add test script	2020-05-19 18:25:18 +01:00
reg019	Add test script	2020-05-19 18:25:18 +01:00
reg020	Make sure literals are normalise on LHS	2020-05-23 11:48:15 +01:00
total001	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
total002	Add test script	2020-05-19 18:25:18 +01:00
total003	All functions now need to be covering by default	2020-05-24 19:58:20 +01:00
total004	Add test script	2020-05-19 18:25:18 +01:00
total005	Add test script	2020-05-19 18:25:18 +01:00
total006	Evaluate with tcinline under Delay	2020-05-22 13:30:07 +01:00
total007	Forgot to add some test files!	2020-05-21 17:22:30 +01:00
total008	More coverage checking fixes	2020-05-24 18:33:43 +01:00
with001	Add test script	2020-05-19 18:25:18 +01:00
with002	Add test script	2020-05-19 18:25:18 +01:00
with003	Apply the patch from idris2-boot.	2020-05-22 20:26:10 +02:00