Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
Am Donnerstag, den 18.09.2014, 15:47 +0200 schrieb Florian Haftmann: Changeset #fe083c681ed8 introduces products over lists. There has been some private discussion whether there could be a serious attempt to establish a new consistent naming scheme for summation and products over collections. a) for lists: sum_list (← listsum), prod_list (← listprod) b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod) c) for finite sets: Sum (← setsum), Prod (← setprod) I assume a) means Sum_list and Prod_list?! Why Sum and not Sum_set in c)? Is the intention that the canonical type always gets the short name? Like map instead of map_list. And why upper case Sum instead of sum? - Johannes PS: Maybe c) could be tackled in the future when we have a hypothetical constant/lemma renaming tool. As far as can be forseen, 58 theories would be affected by a switch as suggested by a). b) is no big issue. c) is maybe beyond what should be reasonably attempted (218 affected theories). Suggestions welcome. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Products over lists – naming convention for big sums and products.
One could argue that sets are the canonical indexing structure. On the other hand, we have syntax to make the actual names irrelevant. Larry On 24 Sep 2014, at 11:18, Johannes Hölzl hoe...@in.tum.de wrote: Why Sum and not Sum_set in c)? Is the intention that the canonical type always gets the short name? Like map instead of map_list. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] distributed installation + sledgehammer file write permissions
Hi, I use Isabelle for teaching and it was installed by an adjustment to the web-distribution for our Linux machines. Now, I will need to use a lab running on Window, s and that created a few issues I couldn’t help our support team much. 1) distributed config setup: Is there any suggested / configuration-setup for distributed installations of Isabelle (Linux or Windows)? The support guy said, for example, the the Window installation asking for a directory would be a problem for an administered install. In the end, I extracted the .exe and built HOL heaps and use that as a starting point to be shared (i.e. in the way Windows lab is setup, that means running a shared copy of Isabelle remotely as local installations aren’t viable). 2) sledgehammer file write access: This worked to a degree, but say, sledgehammer fails saying SysErr because of a file-write problem. Where is it SH is trying to write to? Or in general, what would you suggest to make a distributed Windows installation viable for a teaching lab? This is for Isabelle2014 on Windows 8.1 Many thanks. Best, Leo signature.asc Description: Message signed with OpenPGP using GPGMail ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
