Re: [isabelle] I need a fixed mutable array
On 14-06-18 14:26, Ramana Kumar wrote:
I recommend looking at the other (non-x86) processor models in HOL4
too. Not all are complex and huge (though I guess that depends on your
Thanks for the suggestion. There's always more to say than anyone wants
I'll say the same thing here that I'll say to Peter Lammich about the
info he gave me. It's probably better that I didn't get this information
from you before now. In particular, my finding this link from your tip:
That would be about ARMv7. The ARM Cortex-A15 was the CPU I thought I
was going to go with. Please see  and  below.
There's like three main factors in looking at CPUs: they need to be sold
on a board that's affordable, they need to have a large following, and
they need to have some lasting power.
The Sony Playstation 3 CPU looks great, and it's fairly cheap, but then
the Sony PS4 is changing to an AMD CPU. That's a bad sign.
Basically, there's GPUs, ARM, and Intel i7. Part of my pursuit began
with looking for processors that have 256-bit data registers, because I
used to work in graphics image generators, which had 256-bit wide data
It was there all the time with the i7, and even before for 128-bit, with
SSE, SSE2, SSS3, SS3, SS4, and now it's there for 256-bit, with AVX
RISC and ARM sounds like it should be fast, but then I looked at ,
and it's not like they blow everyone away.
I think an i7 is hard to beat, with 4 cores and 8 threads, with a clock
at 3 to 4 GHz.. Lots of people have them, and people don't have to do
anything special to run them, unlike embedded processors, or external,
single board Linux computers.
All these practical considerations have a big part in influencing what
route I think I should go. ARM is good, but then there's all sorts of
special things I have to do for, among other things, develop tools.
 Samsung Exynos 5 Octa:
 ODROID-X3: ARM Cortex-A15 / Cortex A7 / Samsung Exynos 5 Octa based
computer for $169.
 CoreMark integers tests: http://www.eembc.org/coremark/index.php
(sort by CoreMark/MHz)
 Brix with i7-4770R:
This archive was generated by a fusion of
Pipermail (Mailman edition) and