Hons efficiency in SBCL, hl-hspace-norm-aux #728
Comments
|
Hi, David --
I seem to remember several months ago that after I noted that SBCL
seems faster than CCL in the regression (also in some other tests I've
un), someone (Jared?) pointed out that hons-intensive applications are
likely to do better with CCL, because of the use of static conses (as
you point out).
The backtrace doesn't surprise me but offhand I don't see any
particular way to improve that situation, other than perhaps
increasing the stack size. In your saved_acl2 you'll likely see
…--control-stack-size 64
and you could edit that. For example, I've done this (though I don't
know that you'll need to mess with the existing value of
--dynamic-space-size):
--dynamic-space-size 240000 --control-stack-size 640
-- Matt
"David L. Rager" <notifications@github.com> writes:
[1:text/plain Hide]
SBCL made it through a lot of forms more efficiently than CCL. (e.g., one file with a large defsvtv seems to only take about 65% of the time). That being said, when it comes to proving the types of the associated keys that are returned from an `svtv-run`, sbcl goes out to lunch.
Perhaps it's no surprise that sbcl goes out to lunch in `hl-hspace-norm-aux`, since there are no static conses. That being said, it seems like a reasonable place to begin.
Backtrace:
```
c
c This is glucose 3.0 -- based on MiniSAT (Many thanks to MiniSAT team)
c Simplification mode is turned on
c
WARNING: for repeatability, setting FPU to use double precision
c ========================================[ Problem Statistics ]===========================================
c | |
c | Number of variables: 5 |
c | Number of clauses: 0 |
c | Parse time: 0.00 s |
c | |
c | Eliminated clauses: 0.00 Mb |
c | Simplification time: 0.00 s |
c | |
c ========================================[ MAGIC CONSTANTS ]==============================================
c | Constants are supposed to work well together :-) |
c | however, if you find better choices, please let us known... |
c |-------------------------------------------------------------------------------------------------------|
c | | | |
c | - Restarts: | - Reduce Clause DB: | - Minimize Asserting: |
c | * LBD Queue : 50 | * First : 2000 | * size < 30 |
c | * Trail Queue : 5000 | * Inc : 300 | * lbd < 6 |
c | * K : 0.80 | * Special : 1000 | |
c | * R : 1.40 | * Protected : (lbd)< 30 | |
c | | | |
c ==================================[ Search Statistics (every 10000 conflicts) ]=========================
c | |
c | RESTARTS | ORIGINAL | LEARNT | Progress |
c | NB Blocked Avg Cfc | Vars Clauses Literals | Red Learnts LBD2 Removed | |
c =========================================================================================================
c last restart ## conflicts : 0 0
c =========================================================================================================
c restarts : 1 (0 conflicts in avg)
c blocked restarts : 0 (multiple: 0)
c last block at restart : 0
c nb ReduceDB : 0
c nb removed Clauses : 0
c nb learnts DL2 : 0
c nb learnts size 2 : 0
c nb learnts size 1 : 0
c conflicts : 0 (0 /sec)
c decisions : 1 (0.00 % random) (1001 /sec)
c propagations : 4 (4004 /sec)
c conflict literals : 0 (-nan % deleted)
c nb reduced Clauses : 0
c CPU time : 0.000999 s
s SATISFIABLE
C-c C-c
debugger invoked on a SB-SYS:INTERACTIVE-INTERRUPT in thread
#<THREAD "main thread" RUNNING {10605AF193}>:
Interactive interrupt at #x1001CBA622.
Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.
restarts (invokable by number or by possibly-abbreviated name):
0: [CONTINUE] Return from SB-UNIX:SIGINT.
1: Ignore runtime option --eval "(acl2::sbcl-restart)".
2: [ABORT ] Skip rest of --eval and --load options.
3: Skip to toplevel READ/EVAL/PRINT loop.
4: [EXIT ] Exit SBCL (calling #'EXIT, killing the process).
((FLET #:BODY-FUN-579 :IN SB-IMPL::GETHASH3))
0] sb-debug:backtrace
Backtrace for: #<SB-THREAD:THREAD "main thread" RUNNING {10605AF193}>
0: ((FLET #:BODY-FUN-579 :IN SB-IMPL::GETHASH3))
1: (SB-IMPL::GETHASH3 (SV::BITNOT (SV::BITAND (SV::RSH 6 (SV::CONCAT 1 (SV::BITNOT #) (SV::CONCAT 1 # #))) (SV::RSH 6 (SV::CONCAT 1 (SV::BITNOT #) (SV::CONCAT 1 # #))))) #<HASH-TABLE :TEST EQ :COUNT 293004 {10020C40B3}> NIL)
2: (HL-CACHE-GET #<unavailable argument> #<unavailable argument>)
3: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
4: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
5: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
6: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
7: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
8: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
9: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
10: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
11: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
12: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
13: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
14: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
15: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
16: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
17: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
18: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
19: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
20: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
21: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
22: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
23: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
24: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
25: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
26: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
27: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
28: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
29: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
30: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
31: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
32: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
33: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
34: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
35: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
36: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
37: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
38: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
39: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
40: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
41: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
42: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
43: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
44: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
45: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
46: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
47: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
48: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
49: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
50: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
51: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
52: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
53: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
54: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
55: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
56: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
57: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
58: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
59: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
60: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
61: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
62: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
63: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
64: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
65: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
66: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
67: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
68: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
69: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
70: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
71: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
72: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
73: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
74: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
75: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
76: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
77: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
78: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
79: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
80: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
81: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
82: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
83: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
84: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
85: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
86: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
87: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
88: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
89: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
90: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
91: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
92: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
93: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
94: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
95: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
96: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
97: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
98: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
99: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
100: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
101: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
102: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
103: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
104: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
105: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
106: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
107: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
108: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
109: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
110: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
111: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
112: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
113: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
114: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
115: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
116: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
117: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
118: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
119: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
120: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
121: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
122: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
123: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
124: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
125: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
126: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
127: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
128: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
129: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
130: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
131: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
132: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
133: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
134: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
135: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
136: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
137: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
138: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
139: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
140: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
141: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
142: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
143: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
144: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
145: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
146: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
147: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
148: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
149: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
150: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
151: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
152: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
153: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
154: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
155: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
156: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
157: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
158: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
159: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
160: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
161: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
162: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
163: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
164: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
165: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
166: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
167: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
168: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
169: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
170: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
171: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
172: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
173: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
174: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
175: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
176: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
177: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
178: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
179: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
180: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
181: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
182: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
183: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
184: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
185: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
186: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
187: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
188: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
189: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
190: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
191: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
192: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
193: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
194: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
195: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
196: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
197: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
198: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
199: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
200: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
201: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
202: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
203: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
204: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
205: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
206: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
207: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
208: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
209: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
210: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
211: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
212: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
213: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
214: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
215: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
216: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
217: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
218: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
219: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
220: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
221: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
222: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
223: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
224: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
225: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
226: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
227: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
228: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
229: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
230: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
231: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
232: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
233: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
234: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
235: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
236: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
237: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
238: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
239: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
240: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
241: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
242: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
243: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
244: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
245: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
246: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
247: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
248: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
249: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
250: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
251: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
252: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
253: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
254: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
255: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
256: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
257: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
258: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
259: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
260: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
261: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
262: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
263: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
264: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
265: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
266: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
267: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
268: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
269: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
270: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
271: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
272: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
273: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
274: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
275: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
276: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
277: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
278: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
279: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
280: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
281: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
282: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
283: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
284: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
285: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
286: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
287: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
288: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
289: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
290: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
291: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
292: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
293: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
294: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
295: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
296: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
297: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
298: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
299: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
300: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
301: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
302: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
303: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
304: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
305: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
306: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
307: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
308: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
309: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
310: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
311: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
312: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
313: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
314: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
315: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
316: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
317: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
318: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
319: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
320: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
321: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
322: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
323: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
324: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
325: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
326: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
327: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
328: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
329: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
330: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
331: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
332: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
333: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
334: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
335: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
336: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
337: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
338: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
339: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
340: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
341: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
342: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
343: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
344: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
345: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
346: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
347: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
348: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
349: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
350: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
351: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
352: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
353: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
354: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
355: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
356: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
357: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
358: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
359: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
360: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
361: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
362: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
363: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
364: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
365: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
366: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
367: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
368: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
369: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
370: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
371: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
372: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
373: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
374: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
375: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
376: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
377: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
378: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
379: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
380: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
381: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
382: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
383: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
384: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
385: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
386: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
387: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
388: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
389: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
390: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
391: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
392: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
393: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
394: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
395: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
396: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
397: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
398: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
399: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
400: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
401: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
402: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
403: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
404: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
405: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
406: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
407: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
408: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
409: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
410: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
411: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
412: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
413: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
414: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
415: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
416: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
417: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
418: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
419: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
420: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
421: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
422: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
423: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
424: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
425: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
426: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
427: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
428: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
429: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
430: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
431: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
432: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
433: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
434: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
435: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
436: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
437: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
438: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
439: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
440: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
441: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
442: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
443: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
444: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
445: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
446: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
447: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
448: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
449: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
450: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
451: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
452: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
453: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
454: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
455: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
456: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
457: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
458: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
459: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
460: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
461: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
462: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
463: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
464: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
465: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
466: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
467: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
468: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
469: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
470: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
471: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
472: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
473: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
474: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
475: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
476: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
477: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
478: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
479: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
480: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
481: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
482: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
483: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
484: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
485: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
486: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
487: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
488: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
489: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
490: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
491: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
492: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
493: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
494: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
495: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
496: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
497: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
498: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
499: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
500: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
501: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
502: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
503: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
504: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
505: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
506: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
507: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
508: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
509: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
510: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
511: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
512: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
513: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
514: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
515: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
516: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
517: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
518: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
519: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
520: (HL-HSPACE-NORM-AUX #<unavailable argument> #<unavailable argument> #<unavailable argument>)
521: (HONS-COPY #<unavailable argument>)
522: (RAW-EV-FNCALL #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
523: (EV-FNCALL #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
524: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-FNCALL #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
525: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
526: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-LIST #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
527: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
528: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
529: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-LIST #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
530: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-LIST #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
531: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
532: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
533: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
534: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-LIST #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
535: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
536: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
537: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
538: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-LIST #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
539: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
540: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
541: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
542: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-LIST #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
543: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
544: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TERM-EQUIVS #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
545: (MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TEST #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
546: (ACL2_*1*_ACL2::MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-TOP-LEVEL-TERM #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
547: (ACL2_*1*_ACL2::MY-THIRD-GL-CLAUSE-PROCESSOR-INTERP-HYP/CONCL #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
548: (ACL2_*1*_ACL2::MY-THIRD-GL-CLAUSE-PROCESSOR-RUN-PARAMETRIZED #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
549: (ACL2_*1*_ACL2::MY-THIRD-GL-CLAUSE-PROCESSOR #<unavailable argument> #<unavailable argument> #<unavailable argument>)
550: (RAW-EV-FNCALL #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
551: (EV #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
552: (EV-FOR-TRANS-EVAL #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument> #<unavailable argument>)
553: (EVAL-CLAUSE-PROCESSOR #<unavailable argument> #<unavailable argument> #<unavailable argume
|
|
The "static honsing" scheme used in CCL/GCL is definitely a lot more efficient than the "classic honsing" scheme used in other lisps like SBCL. It's hard to imagine fixing this without either (1) adding static consing to SBCL or (2) replacing "classic honsing" with some new implementation that is somehow better, which is probably hard because writing efficient low-level data structures in Lisp isn't easy. It might be worthwhile to see if the performance difference is really just due to the honsing scheme instead of something else. To do this, you might try rebuilding ACL2 in CCL but after removing This will give you an ACL2 with classic honsing on top of CCL. By comparing this against SBCL, you'll be doing an apples-to-apples comparison. Almost surely CCL will perform badly here, too, when hobbled by classic honsing. If somehow SBCL still isn't competitive, I would suspect the hashing algorithm. Over the years we found a few performance problems with CCL's hash tables, and these issues have been fixed. I don't have any reason to believe SBCL has a similar problem, but when you're honsing a large structure (as in your stack trace) there's really almost nothing else going on other than hashing and consing. |
|
Thanks y'all for chiming in. That's a pretty easy experiment for me to run, now that I know which books go out to lunch. Will do and add it here for the record. My goal for this issue is to serve as a starting point for anyone who becomes motivated to dive into this issue. |
|
Results from running the suggested experiment by building a CCL with no static hons feature and ld'ing one of the books that takes advantage of static honses: got a backtrace very similar to the sbcl backtrace. Thus, we can conclude that the way we use static honses in CCL helps. That's not really surprising. Leaving this issue for now, but at least we are now aware of the concrete problem. Perhaps someone will think of another way to implement it without using static conses. On a related note, Lispworks seems to have some static cons space. Search for "cons-static" at http://www.lispworks.com/documentation/lw70/LW/html/lw-78.htm I won't post all of the backtrace, but here's the 0th frame: |
|
David, did you try my suggestion of something like this in your saved_acl2? Or, if you can tell me how to reproduce the problem, I could give it a try. |
|
Hi Matt,
Thanks for the idea. I had to interrupt ACL2 (as opposed to experiencing a
stack overflow), so I'm currently doubtful that changing the stack sizes
would matter. If you know something to change my mind, though, please lmk!
Thanks,
David
…On Thu, Jun 1, 2017 at 11:31 AM, MattKaufmann ***@***.***> wrote:
David, did you try my suggestion of something like this in your saved_acl2?
--dynamic-space-size 240000 --control-stack-size 640
Or, if you can tell me how to reproduce the problem, I could give it a try.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#728 (comment)>, or mute
the thread
<https://github.com/notifications/unsubscribe-auth/ACJE_hGxL7SeyAiBlne9xz4TRNryNHSqks5r_udygaJpZM4Notb7>
.
|
|
Hi, David --
Ah -- OK, right, my suggestion probably wouldn't help. (I'm not 100%
sure of that, though -- for all I know SBCL got into a weird
stack-overflow state and your interrupt just woke it up.)
…-- Matt
"David L. Rager" <notifications@github.com> writes:
[1:text/plain Hide]
Hi Matt,
Thanks for the idea. I had to interrupt ACL2 (as opposed to experiencing a
stack overflow), so I'm currently doubtful that changing the stack sizes
would matter. If you know something to change my mind, though, please lmk!
Thanks,
David
On Thu, Jun 1, 2017 at 11:31 AM, MattKaufmann ***@***.***>
wrote:
> David, did you try my suggestion of something like this in your saved_acl2?
>
> --dynamic-space-size 240000 --control-stack-size 640
>
> Or, if you can tell me how to reproduce the problem, I could give it a try.
>
> —
> You are receiving this because you authored the thread.
> Reply to this email directly, view it on GitHub
> <#728 (comment)>, or mute
> the thread
> <https://github.com/notifications/unsubscribe-auth/ACJE_hGxL7SeyAiBlne9xz4TRNryNHSqks5r_udygaJpZM4Notb7>
> .
>
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
SBCL made it through a lot of forms more efficiently than CCL. (e.g., one file with a large defsvtv seems to only take about 65% of the time). That being said, when it comes to proving the types of the associated keys that are returned from an
svtv-run, sbcl goes out to lunch.Perhaps it's no surprise that sbcl goes out to lunch in
hl-hspace-norm-aux, since there are no static conses. That being said, it seems like a reasonable place to begin.Backtrace:
The text was updated successfully, but these errors were encountered: