--- layout: post title: '\"Track changes\" in weblogs?' date: 2005-01-25 00:00:00 ---
I'd never noticed NetNewsWire doing this before:
Is it really noticing changes between versions of a story in an RSS feed and highlighting said changes? If so - WOW. If the Guardian have the honesty to be driving this process in any way: WOW.


Activists Toolkit
For a militant digital resistance!Work in progress!
Having weak passwords defeats all encryption - it is obvious that you need to use strong passwords. But at the same time you should never use the same password for different purposes. We recommend you to have only a couple of strong passwords memorized, for things like disk encryption, password manager and gpg-key. All the other passwords (facebook, mail, ...) can be stored in a password manager like KeePassX. As method for generating strong passwords you can use Diceware.
Examples for bad passwords:
- :LOL1313le
- Coneyisland9/
- momof3g8kids
- 1368555av
- n3xtb1gth1ng
- qeadzcwrsfxv1331
- m27bufford
Generating strong passwords using Diceware method
You need a dice and a big wordlist. (This is a new good wordlist by EFF) To create your password stick seven (or more) random words from this list together. For each word you have to roll your dice five times, write down the resulting digits and look them up in the wordlist.
This creates passwords like siblingsurveybullfrogjestercobwebduvettasting.
- Start or restart Tails in non-persistent mode.
- Open the Terminal. Then copy and paste the following code into the Terminal. To confirm press Enter.
curl --socks5-hostname <IP_ADDRESS>:9050 -s https://www.eff.org/files/2016/07/18/eff_large_wordlist.txt | shuf -n 7 -r --random-source /dev/random
- Important: Shut down Tails immediately without doing anything else.
Installing KeePassX on Linux Mint
- Open the start menu and press the button to start Software Manager. Enter your password.
- Type
KeePassX
into the search box in the top right of the window, then press Enter. - Double click onto Keepassx and click the button Install.
- Start KeePassX and click on Database > New Database in the top menu.
- Choose a strong master password (Diceware!) and click OK.
- Save the new database by clicking Database > Save Database in the top menu.
Worth Mentioning
- Subgraph OS - An operating system built for anonymized and secure communication. Is still being developed, but could replace Linux Mint in the future.
- Qubes OS - A "resonably" secure operating system, but needs a big change in how you use the computer. Recommended for more advanced users.
Installing Linux Mint
- Download Linux Mint from linuxmint.com. If you have a fairly modern computer choose the Cinnamon 64-bit edition. If your computer is older and lags running windows choose the Xfce 32-bit edition.
- Verify that nobody has tampered the downloaded iso file. This step is very important, do not skip!
- Windows:
- Download and install Gpg4win.
- Download the two files on linuxmint.com/verify.
- Open Kleopetra, which got installed with Gpg4win.
- [TODO] Recive key
27DE B156 44C6 B3CF 3BD7 D291 300F 846B A25B AE09
- [TODO]
- Burn the downloaded iso file to an empty usb stick.
- Linux:[TODO]
- Windows: Download and use the software Rufus with the default settings.
- Mac: Just right-click on the file and choose
Burn Disk Image
- Boot from the USB stick. For instructions on how to do that just search for "boot from usb stick [computer model you use]".
- Follow the instructions on the screen to install Linux Mint.
Important: On the forth page of the installer make sure to choose the option
Encrypt the new Linux Mint installation for security
Basic settings for Linux Mint
To get all updates it is important that you choose Always update everything as update policy in the Update Manager. Your system will still be stable, even if this option is "officially" only recommended for experienced users.
Browsing with the Tor Browser hides your browsers fingerprint and your computers IP address, which authorities could use to get your real address. But you still have to take care to not accidentally reveal your identity by posting personal information on the internet.
You can get a new anonymous identity by clicking the Tor icon in the address bar and selecting New Identity. We recommend you to do this relativly often, at least each time the subject of your internet research changes. (From planning a direct action to reading the news for example.)
Installing Tor Browser Launcher on Linux Mint
- Open the Terminal (Linux Mint: in the bar on the bottom left). Then type the following statements and press Enter after each one.
sudo add-apt-repository ppa:micahflee/ppa
sudo apt-get update
sudo apt-get install torbrowser-launcher
- Click the Tor icon in the address bar and click Security Settings.
- Turn the Slider to Medium (for High continue reading).
Using NoScript (with Tor Browser)
JavaScript is a technology most websites use to show dynamic content. But having JavaScript enabled makes your browser more vulnerable to attacks which could reveal your real IP and compromise your computer. Because of that we recommend that you disable JavaScript in the Tor Browser and only enable it temporarily for websites you trust.
- Click the Tor icon in the address bar and click Security Settings.
- Turn the Slider to High. This disables JavaScript on all websites.
If you want to enable JavaScript temporarily for the website you are visiting:
- Click the NoScript icon in the address bar and select Temporarily allow all this page.
Firefox (without Tor)
Install these addons to make Firefox a bit safer to use:
- HTTPS Everywhere
- uBlock Origin
- Decentraleyes
NoScript- NoScript might be overkill if you use this Browser only for the few websites connected to your real identity.
We recommend Thunderbird as email client available for Linux, Windows and Mac.
To protect your identity it can make sense to have two (or more) different email addresses. One is connected to your name, to your work, family, etc. The other one is created anonymously through Tor Browser. To preserve the anonymity you have to use TorBirdy to run Thunderbird through Tor.
Thunderbird Profiles
If you want to use Thunderbird for both your official and your anonymous identity you can create a second Profile in Thunderbird. That way each time you start the application it asks what profile it should use. With profiles you get complete separation of the email accounts, the addressbook and the installed plugins.
-
To create a second profile you need to open the profile manager:
- Linux: Open the Terminal (Linux Mint: in the bar on the bottom left). Type
thunderbird -P
and press Enter . - Windows: Select
Start > Run...
from the Windows Start menu. Enterthunderbird -P
and pressOk
. [TODO][Not verified!] - Mac: Open the Console. Type
/Applications/Thunderbird.app/Contents/MacOS/thunderbird-bin -profilemanager
and press Enter .
- Linux: Open the Terminal (Linux Mint: in the bar on the bottom left). Type
-
Uncheck the checkbox next to
Use the selected profile without asking at startup
to be able to choose between profiles at startup. -
Press
Create Profile...
and follow the instructions. -
Make sure the new created Profile is selected and press
Start Thunderbird
to begin setting up your new Profile.
Thunderbird Addons
Along with Thunderbird you should install several Addons. (If you created a second Profile you have to install this Addons only in that new Profile.)
- To open the addon manager press the toolbar entry and press
Add-ons
. - To install each of the following Addons enter the addon's name into the search box and click on
Install
- Restart Thunderbird for the changes to take effect.
Thunderbird Account Settings
[TODO]
Privacy-Conscious Email Providers
Jabber + OTR (Off-the-record encryption) is the equivalent to Email + PGP for chatting. You can choose between different applications on your computer and smartphone to use it. OTR similar to PGP provides End-to-End encryption. This means, that even the server you use to communicate with others can not read your messages. Different to Email both parties have to be online and (with Tor Messenger) per default no chat history is saved.
Installing Tor Messenger on Linux
- Open this link to the website of Tor Messenger. Download and save the Linux (64-bit) version of Tor Messenger and both files starting with sha256sums to your Downloads directory.
- Open the Terminal (Linux Mint: in the bar on the bottom left). Then type the following statements and press Enter after each one.(Hint: If you feel lazy you can complete filenames by pressing Tab.)
cd Downloads
gpg --keyserver keys.gnupg.net --recv 6DA77FAA
gpg --verify sha256sums-signed-build.txt.asc
The output should contain the line gpg: Good signature from "Sukhbir Singh<EMAIL_ADDRESS>fingerprint in the last line should match E4AC D397 5427 A5BA 8450 A1BE B01C 8B00 6DA7 7FAAsha256sum -c sha256sums-signed-build.txt 2>/dev/null | grep OK
The output should end with OKrm tor-messenger*
gpg --delete-keys --yes --batch 6DA77FAA
tar -xvaf tor-messenger* -C ~
cd ~/tor-messenger
./start-tor-messenger.desktop --register-app
- Press the button in the start menu to logout. After you have logged in again, you should be able to start Tor Messenger from the start menu. The software checks for updates every time it is run and installs updates automatically. Congrats, now it is time to create a jabber account and start messaging!
You have now verified that your download of Tor Messenger has not been manipulated. If some of the commands produced not the expected output it might be possible that you are being attacked.
In that case delete all downloaded files by typing the commands:
Then try everything again from a different location or internet access point.
Configuration of Tor Messenger
- Start Tor Messenger and connect to the Tor Network.
- In the Account Wizard window choose XMPP as protocol.
- Open the Tor Browser to create a new Jabber account. We recommend systemli as provider, but they are by far not the only ones. In the Tor Browser open the address https://jabber.systemli.org:5281/register_web and fill out the form.
- Back in the Tor Messenger application enter your chosen username into the username field and
jabber.systemli.org
into the domain field. (If you choose to register with systemli.) - In the next window just enter your password and click Next.
- Click onto XMPP Options to show the advanced options. When you scroll the window down a bit you should see a field with the name Server. Here you can enter the address of a hidden server, if your Jabber provider supports this. For systemli accounts enter
x5tno6mwkncu5m3h.onion
and press Next and finish the account wizard. - Tor Messenger does never autoconnect, click on Connect.
- If you did input a hidden server and connect for the first time: There will be a security warning: requested domain name does not match the server's certificate. This time and only this time press Add Exception and click Confirm Security Exception.
- As last thing we recommend you to right-click into the empty Tor Messenger window (not the accounts window) and select Show Offline Contacts.
Chatting with Tor Messenger
To start chatting with a contact over jabber you need to add them to your contact list. For that you need their jabber address. It looks like an email adress, for example<EMAIL_ADDRESS>- In the top menu click on File > Add Contact...
- Type your contacts address into the username field and click Ok
- Your contact gets a message where they have to allow your contact request. If they accept, the contact should not be greyed out in your contact list anymore.
- To start a chat double-click onto the new contact and send a message.
- You could start chatting now, but wait. To be sure that you are not being eavesdropped it is critical that you verifiy your contacts identity. Click on Verify in the chat window and follow the instructions on the screen.Only if the small lock symbol in the upper right corner of the chat window is green can you be sure that the chat is properly secured.
Small hint: If you are the one getting a contact request there is one more thing you should do after you clicked on Allow and your contact texted you. In the chat window right-click on your contacts jabber address and click Add Contact... > Contacts. Only then can you see your contacts online status.
Mobile clients
Conversations
Conversations supports not only OTR encryption but the supperior OMEMO encryption. The problem is only, that right now there is no Desktop application capable of OMEMO in a safe way.
Download conversations in the F-Droid appstore if you can not pay for the software. (But please support the developers if possible!)
Available for: Android
Guides
- Surveillance Self-Defense by EFF - Guide to defending yourself from surveillance by using secure technology and developing careful practices.
- Email Self-Defense by FSF - A guide to fighting surveillance with GnuPG encryption.
OpSec (Operational Security)
- Clandestine Mobile Phone Use (1)
- Clandestine Mobile Phone Use (2)
- Tools to evade stylometrics
- Using Codes
Information
- Surveillance Industry Index - Database of surveillance products.
- Freedom of the Press Foundation - Supporting and defending journalism dedicated to transparency and accountability since 2012.
Tools
- Fake Name Generator - Generate a random identity, with full address, phone number and more.
- ipleak.net - IP/DNS Detect - What is your IP, what is your DNS, what informations you send to websites.
- PRISM Break - We all have a right to privacy, which you can exercise today by encrypting your communications and ending your reliance on proprietary services.
- Security in-a-Box - A guide to digital security for activists and human rights defenders throughout the world.
- AlternativeTo.net - Great collection of open source online and self-hosted software sorted by likes.
- SecureDrop - An open-source whistleblower submission system that media organizations can use to securely accept documents from and communicate with anonymous sources. It was originally created by the late Aaron Swartz and is currently managed by Freedom of the Press Foundation.
- Reset The Net - Privacy Pack - Help fight to end mass surveillance. Get these tools to protect yourself and your friends.
- Security First - Umbrella is an Android app that provides all the advice needed to operate safely in a hostile environment.


User Information
Nickname
Alternative
Name
Email
Notifications
Notifications for Private Messages
Notifications for Channel Messages
Save
Cancel


--- layout: archive title: Zulip Chat Archive permalink: /stream/113488-general/topic/Travis.html ---
Travis is complaining on my PRs #883 and #897, but I am not sure this is my fault: what is failing is the shell tests "check install scripts" and "check dev scripts". Is there anything I can do about it?
I conjecture it's something to do with pushing from your own fork instead of a branch of leanprover-community. @Simon Hudon 's working on fixing it. I guess #883 can probably safely be merged, and it will build once it's on master.
@Sebastien Gouezel can you push your branches to leanprover-community/mathlib
? It makes it easier to test the installation scripts that way because GitHub rejects requests when you make more than a few without authentication.
Travis is timing out on completely innocent pull requests, like #1423.
Does anyone know which commit caused this regressed behavior?
I saw that other Github repo's automatically got a reply with compilation performance. Maybe we can make a bot that automatically replies to a PR if the compilation time is increased by more than 5% or something?
I assumed in my previous message that there was a merged commit that caused performance issues, but they all seem fine. Maybe this was a cache-related issue (I merged the PR into master, maybe that fixes it)
Regardless of what caused it here, regression testing for compilation time would be a good idea.
I don't know if Travis is reliable enough to do this.
But maybe we could run something once a day on Scott's server?
I guess that would more reliably throw the same processing power at it.
Last three pushes to master built in around 107 (most recent), 100, 110 minutes. I didn't look at the changes, but I assume they were not responsible for this variance.
Interestingly this build of PR #1428 timed out, but leanpkg build
actually finished, it just took so much longer than usual that there wasn't enough time left to run leanchecker
.
I'm sure a dedicated machine would be more consistent, I'm not sure how much more consistent.
Doesn't Scott already build everything anyways? Or did I imagine that?
I think the mathlib nightlies get pushed to Scott from Travis. Would he be building for another reason?
I could be wrong about that though.
No, at present I'm still building nothing. That project fell through, for lack of anyone who had the time/expertise combination to script things. I think the idea had been to push from travis to my account on S3, and then for my computer to poll that S3 account, but the pushing-to-S3 step never happened.
I would love to have the infrastructure in place so that every commit received an olean cache. I can provide the CPU time, I think.
I think that's @Simon Hudon 's territory. Checking build times once a day would be a lot simpler. Do you think your server has a consistent enough load to do this with enough precision?
Probably. It has 18 physical cores. I routinely leave some single-threaded calculations running, but it's never more than 6. It's been a while since I've had anything multithreaded that I want left running. So if I limit the build to say 6 or 8 cores, and run it in the middle of my night, it shouldn't have any competition.
The idea is that I would just pull a fresh copy of master, build, and have a script post the time here?
Yeah, something like that. We just want to see an alert if there's an unexpected jump in compile time. Posting here would be enough.
Ideally, if it noticed a spike it would try to find the responsible commit.
That could use a bunch more cycles.
I think our limiting factor is scripting and testing, not available cycles.
I am just capable enough at writing bash scripts to do a bad job of this, so help would definitely be appreciated. It might require jumping through some hoops, but I could probably work out how to give someone ssh access.
Feel free to put that code up on mathlib-tools
and I'll see if I can contribute something
@Simon Hudon, I'm helpless at this, it seems. I downloaded zulip's sample python file for posting a message from https://leanprover.zulipchat.com/api/send-message, as scripts/zulip.py
. I ran pip install zulip
, which seemed to work. However running ./zulip.py
just says:
idaeus:scripts scott$ python zulip.py Traceback (most recent call last): File "zulip.py", line 1, in <module> import zulip File "/Users/scott/projects/lean/mathlib-tools/scripts/zulip.py", line 4, in <module> client = zulip.Client(config_file="~/.zuliprc") AttributeError: 'module' object has no attribute 'Client'
which suggests to me that python is not correctly finding the zulip library.
(I've committed the sample script to mathlib-tools
, so you can see what I'm trying to do.)
I tried some variations, e.g. pip3 install zulip
, and it reports success too. :-)
(If my computer can't even work out how to run a little shell script, how on earth is it going to get a gold medal at the IMO...?!)
I'm sure there are a lot of IMO gold medalists that down know what a bash script is...
Cancel this request for help, I found zulip-send
, which just works from the command line.
I can also put together some shell scripts, especially if you can figure out a way to grant me access to your machine
I was thinking it might be nice to run lean --profile
with these regular builds of mathlib to get more detailed diagnostics. However, I tried running lean --make --profile src/ > profile.log
in my mathlib directory and it keeps segfaulting after a while. Has anyone tried anything like this?
I also meant to ask whether there are statistics (lean --profile
or anything else like it) which would be good to record and don't affect compile time too much
I managed to profile mathlib with lean -j1 --make --profile src/ > profile.log
. It took maybe 2 hours on my machine, so it's probably not something we could run more than once a day:
cumulative profiling times: compilation 12.8s decl post-processing 2.56e+03s elaboration 3.87e+03s elaboration: tactic compilation 70.9s elaboration: tactic execution 2.67e+03s parsing 122s type checking 17.2s
I've attached the (compressed) profile.log
if anyone else wants to have a go at extracting useful statistics from it: profile_140a606.log.zip (3.1MB)
Couldn't we run it 12*N times per day, if we have N processors?
(Assuming we believe in isolation between processors which is definitely false, but hey)
It also used a fairly large amount of memory too (~2 GB by the end).
I have 128gb on this machine, so memory shouldn't be a problem.

A student has been running calculations in GAP that use lots of RAM, but simultaneously I started experimenting with building Lean regularly via cron, so I don't really know which is at fault.
I've also been having trouble getting my build script to run multithreaded.... Usually Lean uses lots of cores, but somehow when it runs in the cron job, it uses 2 cores for a few minutes, then drops to 1, and I'm completely bamboozled as to why.
@Reid Barton, in terms of giving you (or @Simon Hudon) access to this computer, I think the options are:
1. We fill out the "campus visitor" form, which would give you an ANU id number. I then get our IT people to add that id number to our VPN configuration. To ssh in, you'd then need to connect to the relevant VPN, then ssh.
2. I make a persistent outbound ssh tunnel to some other server (e.g. the one hosting my website), that forwards traffic back to port 22 here. Dodgy as anything, but that's what they invented ssh tunnelling for, I guess.
It's a bit of a hassle either way.
1. looks simpler to me. It also looks less likely you'll get reprimanded for it.
Okay, I have just initiated our process to give both you and Reid university id's here. You'll receive an email with a link to a form, but feel free to fill out the barest minimum of information it will let you submit with. :-)
Cool :)
Sorry I'm not too verbose today. I'm exhausted
Is "suburb" what you call a city?
I guess. :-)
By Australian standards, clearly Berkeley is part of San Francisco, and thus we have very few "cities", so apparently "suburb" is the next division down.
Couldn't we run it 12*N times per day, if we have N processors?
(Assuming we believe in isolation between processors which is definitely false, but hey)
I tried this once, and the conclusion was that sadly if you want to get reliable benchmark results, you need to run your program with pretty much exclusive access to the machine (and on real hardware as opposed to a cloud vCPU). Running one benchmark per physical CPU core skews the timings to the point of uselessness, probably due to contention on memory, on I/O, and whatever else is shared between CPUs. Anyway in case of mathlib, because the build times are so long, maybe random noise is not that much of an issue - unless it's possible for a single run of lean --make
to somehow get in a failure mode which makes the entire build proceed slower than usual, but that seems unlikely.
Yeah, I'm pretty disappointed by the results from overnight.
113m51.476s
113m18.228s
114m49.561s
110m48.239s
105m30.344s
101m58.073s
I would guess that's too much random variability to be useful.
What conditions is that under?
Travis or your own machine?
1 core?
This is on my own machine, running with -j1
.
I realise now that I left it running every hour, so builds were overlapping. I've slowed down cron and will see if that improves things.
If no one else is already working on it I'll take a stab at writing a Python script to parse the profile output into JSON (or some other format?) later tonight.
Now that the builds are not overlapping, the timing is quite uniform ---
98m31.200s
98m52.938s
99m3.707s
99m7.776s
98m57.582s
98m42.635s
98m45.471s
However this has been running over the weekend, without anything else running on this machine. We'll have to see if it stays uniform tomorrow once I'm in the office.
@Bryan Gin-ge Chen if you feel like parsing the profile output into something useful that might be fun. :-)
My script keeps uploading the logs.
top 100 items:
62.4 decl post-processing of lattice.semilattice_sup_top took 62.4s 61.2 decl post-processing of subtype.comm_group took 61.2s 59.3 decl post-processing of is_subgroup.of_div took 59.3s 46.6 decl post-processing of to_monoid_hom took 46.6s 34.8 decl post-processing of image_subgroup took 34.8s 27.8 decl post-processing of list_prod_apply took 27.8s 25.7 decl post-processing of subset_closure took 25.7s 25.4 decl post-processing of closure_subset took 25.4s 24.6 elaboration of monoidal_of_has_finite_coproducts took 24.6s 23.3 decl post-processing of group took 23.3s 23.2 decl post-processing of subtype.group took 23.2s 22.4 decl post-processing of open_subgroup.has_coe took 22.4s 22.1 decl post-processing of continuous_multiset_prod took 22.1s 21.9 decl post-processing of exists_list_of_mem_closure took 21.9s 21.8 elaboration of monoidal_of_has_finite_products took 21.8s 18.9 decl post-processing of image_pointwise_mul took 18.9s 18.8 decl post-processing of image_closure took 18.8s 18.6 decl post-processing of pointwise_mul_monoid took 18.6s 18.1 decl post-processing of inv_ker_one took 18.1s 16.8 decl post-processing of subtype.monoid took 16.8s 16.7 elaboration of functoriality_is_right_adjoint took 16.7s 16.6 decl post-processing of ker_lift_mk' took 16.6s 16.3 elaboration of functoriality_is_left_adjoint took 16.3s 16.1 decl post-processing of ker_lift took 16.1s 15.9 decl post-processing of map took 15.9s 15.5 decl post-processing of is_subgroup.coe_inv took 15.5s 15.5 decl post-processing of preimage_pointwise_mul_preimage_subset took 15.5s 15.4 decl post-processing of closure_subgroup took 15.4s 15.2 elaboration of prod_filter_range_p_mul_q_div_two_eq_prod_product took 15.2s 15.1 decl post-processing of mem_pointwise_one took 15.1s 14.8 elaboration of quadratic_reciprocity took 14.8s 14.6 decl post-processing of ext took 14.6s 14.4 decl post-processing of multiset_prod_apply took 14.4s 14.3 elaboration of simple_func_sequence_tendsto took 14.3s 14.2 decl post-processing of normal_in_normalizer took 14.2s 14.1 elaboration of has_sum_sigma took 14.1s 13.9 decl post-processing of continuous_on.mul took 13.9s 13.9 decl post-processing of prod took 13.9s 13.7 decl post-processing of tendsto_multiset_prod took 13.7s 13.7 elaboration of exists_preimage_norm_le took 13.7s 13.7 decl post-processing of exists_list_of_mem_closure took 13.7s 13.6 decl post-processing of lift_mk took 13.6s 13.6 decl post-processing of closure.is_submonoid took 13.6s 13.6 decl post-processing of pointwise_mul_eq_Union_mul_left took 13.6s 13.6 decl post-processing of refl took 13.6s 13.6 decl post-processing of inj_of_trivial_ker took 13.6s 13.4 elaboration of CommRing_yoneda took 13.4s 13.4 decl post-processing of normal_iff_eq_cosets took 13.4s 13.3 decl post-processing of subtype_val.is_group_hom took 13.3s 13.3 decl post-processing of finset_prod_apply took 13.3s 13.2 decl post-processing of closure_singleton took 13.2s 12.9 elaboration of cocones_iso took 12.9s 12.8 decl post-processing of pointwise_mul_semigroup took 12.8s 12.7 decl post-processing of closure took 12.7s 12.2 decl post-processing of coe.is_group_hom took 12.2s 11.9 decl post-processing of coe_inf took 11.9s 11.8 decl post-processing of mem_closure took 11.8s 11.8 decl post-processing of le_iff took 11.8s 11.7 decl post-processing of pointwise_mul_eq_Union_mul_right took 11.7s 11.5 decl post-processing of mem_closure_union_iff took 11.5s 11.4 elaboration: tactic execution took 11.4s 11.3 decl post-processing of empty_pointwise_mul took 11.3s 11.3 decl post-processing of symm took 11.3s 11.3 elaboration: tactic execution took 11.3s 11.2 decl post-processing of pointwise_mul_empty took 11.2s 11.2 decl post-processing of inhabited took 11.2s 11.1 decl post-processing of eq_trivial_iff took 11.1s 11.1 decl post-processing of continuous_subgroup took 11.1s 11.1 elaboration of map_integral took 11.1s 11.1 decl post-processing of mul_left took 11.1s 11.1 decl post-processing of pointwise_mul took 11.1s 11.1 decl post-processing of ext' took 11.1s 10.9 decl post-processing of mem_norm_comm took 10.9s 10.8 decl post-processing of comm_monoid took 10.8s 10.8 decl post-processing of map_one took 10.8s 10.5 elaboration of cones_iso took 10.5s 10.2 elaboration of exists_subgroup_card_pow_prime took 10.2s 10.2 elaboration of lintegral_eq_nnreal took 10.2s 10.1 decl post-processing of inv_ker_one' took 10.1s 10.1 decl post-processing of singleton.is_mul_hom took 10.1s 10.1 decl post-processing of closure_mono took 10.1s 9.91 decl post-processing of injective_ker_lift took 9.91s 9.86 decl post-processing of continuous_monoid took 9.86s 9.74 decl post-processing of prod_map_range_index took 9.74s 9.71 decl post-processing of tendsto_list_prod took 9.71s 9.58 decl post-processing of one_ker_inv' took 9.58s 9.56 elaboration of unique_diff_within_at.eq took 9.56s 9.5 decl post-processing of open_subgroup took 9.5s 9.49 decl post-processing of inv_iff_ker' took 9.49s 9.47 decl post-processing of inj_iff_trivial_ker took 9.47s 9.44 decl post-processing of prod_zero_index took 9.44s 9.38 decl post-processing of image_closure took 9.38s 9.38 elaboration: tactic execution took 9.38s 9.37 decl post-processing of subtype_mk.is_monoid_hom took 9.37s 9.2 elaboration: tactic execution took 9.2s 9.15 decl post-processing of lift took 9.15s 9.07 elaboration of glue_dist_triangle took 9.07s 9.06 decl post-processing of continuous_group took 9.06s 9.06 elaboration: tactic execution took 9.06s 9.03 decl post-processing of closure_subset_iff took 9.03s
but there is a bit fishy going on; I suspect the times there do not actually reflect the time
On Lines<PHONE_NUMBER>42 we have:
elaboration of subtype.comm_group took 670ms type checking of subtype.comm_group took 0.786ms compilation of subtype.comm_group took 2.67ms
and then suddenly on Line 271385:
decl post-processing of subtype.comm_group took 61.7s
How long did everything in the lines in between take? Is the decl post-processing
for some reason being deferred, and the report time is wall time, including all the work on other things that happened in between?
@Kenny Lau I have looked into this a few weeks ago, and I'm almost certain that "type checking .. took" is incorrect - see #58. I'm not sure about the other timings (elaboration, compilation) though.
Here's a python script that does some minimal parsing of these log files into JSON format: https://gist.github.com/bryangingechen/005e51814e698f889a76b59da0e58852
The JSON files consist of an array of key-value pairs, which mostly correspond to individual lines of the log files (except for elaboration / tactics, which I tried to group together). As a simple example, the following lines:
parsing took 0.117ms elaboration of integral took 63.5ms type checking of integral took 0.289ms compilation of measure_theory.integral took 0.00211ms decl post-processing of integral took 0.932ms
become:
[{ "type": "pars", "t": 0.117 }, { "type": "elab", "lines": [], "t": 63.5, "decl": "integral" }, { "type": "tc", "t": 0.289, "decl": "integral" }, { "type": "comp", "t": 0.00211, "decl": "measure_theory.integral" }, { "type": "decl", "t": 0.932, "decl": "integral" }]
I didn't try too hard to group things together further – if there are other things I should do please let me know.
The JSON files turn out to be ~35MB compared to the ~25MB of the logs. Here's one corresponding to this log in the Travis stream. profile_81a31ca.json.zip (3.1MB)
Based on https://travis-ci.org/leanprover-community/mathlib/jobs/602292786?utm_medium=notification&utm_source=github_status, I'm guessing the Travis config in #1606 isn't right. I wanted to reuse the olean files from the build to run a final test. That test takes ~45 seconds on my laptop and has been going for 20 min on Travis, so I'm guessing it's recompiling everything. I tried to copy the setup for archive and test, which do use the oleans -- any ideas?
My guess is that this is because the master branch was updated after the travis build started. My understanding is that each build stage does a merge with master when it starts, so this can lead to later stages having to do rebuilds.
What? Every build stage does a merge with master? That can't be right. It's testing the PR, not the PR's compatibility with master.
Yes, this surprised me at first too. But see https://travis-ci.org/leanprover-community/mathlib/jobs/602292786#L164 and https://docs.travis-ci.com/user/pull-requests/#my-pull-request-isnt-being-built
If that's what it's doing, I'm very confused about our CI, heh.
But the archive task ran the same command, and finished in a minute. I don't think https://github.com/leanprover-community/mathlib/commit/3f8a492bfa4ba2ad0ff26c3bff298e3afb05f861 landed in between the two.
You're right that the commit happened earlier, so I'm not sure why the docs and archive stages didn't require a rebuild.
@Simon Hudon Do you know what's up here?
I do see wildly different build times for the archive in the PR history, which is consistent with oleans from the first step being invalidated by a merge.
If this is what's happening, it sounds both inefficient and unreliable.
My understanding is that each build stage does a merge with master when it starts, so this can lead to later stages having to do rebuilds.
Where's my upside-down light bulb emoji
Ah. Perhaps one relevant line is this? https://github.com/leanprover-community/mathlib/blob/master/.travis.yml#L14
Edit - never mind, everything in the last step is happening in src
.
Sometimes, it's enough to just restart the travis build
we might also want to try the build of test and archive with touching all the olean
files in src
Because each stage is a whole new build, you restore the cache and clone the git repo and there the time stamps can be unreliable.
Okay, I restarted the build. #1565 should hit master while this is going, so let's see if the same issue comes up.
Should we just add the command to touch all oleans in src? It can't hurt.
It also wouldn't hurt to remove --make
when we build the archive and tests.
If each stage does a fresh merge with master, how do the first stages even work? What if a commit lands during pre-build 2? Doesn't that mean all the work has to be redone in the test stage?
Doesn't that mean all the work has to be redone in the test stage?
I think so, doesn't it explain the spread in run times for the test stages?
I thought the reason we had the pre-build stages was because we were hitting time limits when we built the whole thing in one stage. If we were doing that in the test stage, shouldn't we hit the same limits?
I think we do sometimes, but people often restart the jobs when they fail.
It feels like that should be way more common. I guess commits near the leafs of the import hierarchy would have less of an effect, maybe that limits it.
My mind is blown, and not in a good way, heh.
We could move the linting test to the test stage. That would create less potential duplication of work.
But then maybe we should move archive and docs too? Neither is slow, unless the oleans are outdated.
What do you mean by move docs and archive?
The docs and archive stages of the Travis build. If we build those directories as part of the test stage, instead of as separate stages, there's no chance that updates to master will invalidate the oleans.
Updates to master has no effect on the build. That's not what the issues are
The state of the cache and the timestamps on the files is where you should look for the issues.
This does sound more plausible, though I'm having trouble constructing a mechanism under which recompilation sometimes happens, but usually not.
Could it have to do with the cache being shared between concurrent builds?
Updates to master has no effect on the build.
Are you sure about this? I thought this line would mean that a merge happens at the start of each stage, but maybe my git / github understanding is wrong.
Which line do you mean?
$ git fetch origin +refs/pull/1606/merge:
line 164, it should be highlighted
In particular I thought the suffix /merge
retrieves a merge commit from the PR branch to master.
I can't find any official documentation about the /merge
ref, but I did find this forum post in which someone quotes Github support as saying:
The /merge refs that are being used here are an undocumented feature and you shouldn’t be relying on them. That feature was build to power Pull Requests in the Web UI, it was not built to be used by 3rd party services. Because it’s undocumented – you should not have any expectations about behavior, the behavior might change at any time and those refs might completely go away without warning.
After some testing on my own fork... maybe the +refs/pull/*/merge
branches are fixed to merge with whatever master was at the time of the last commit on the PR branch?
It makes a merge with something, but it doesn't seem to be current master, yeah.
I tried with #1540 and it gave me a merge with the commit containing #1584. I don't see how these are related yet.
If I'm reading the forum post correctly, it seems that the /merge
ref gets updated only when needed by the web UI? Disturbing.
Instead, the mergeability is triggered when it’s needed: when a user visits the page for the pull request via the UI or requests the pull request via the API. In order to determine the mergeability of a pull request, GitHub actually performs a merge between the head and the base ref, and the result of that merge is stored in the /merge ref (the ref you’re using).
git tells me the latter commit is also sgouezel/master
but I'm assuming that's not relevant :)
Oh hey, it gave me a merge with current master this time.
Possibly because you or I clicked on the PR page for #1540 and that triggered an update?
Presumably
And it seems plausible that the last time anyone looked at that page was 2 days ago
So, that's pretty terrible
So basically, Travis is choosing at random what to build every time.
Is this /merge
stuff built in to Travis or something we configured?
Including on the final builds for Mergify.
mergify doesn't build the same commit it will push? I thought that was part of the point
I think it's built into travis. Maybe we will have to look into other CI services?
It's not in the .travis.yml file. Maybe it's configured somewhere I don't have access to?
^ @Mario Carneiro (?)
Hmm, actually, I'm not sure about Mergify. It merges the PR into master and lets Travis build that. Travis is... maybe... checking the merge of that with something else? Does Mergify's merge commit force the /merge
branch to update?
I'd hope that adding a commit to the PR would update /merge
to merge with the current master.
Hopefully the commit mergify builds will be a descendant of current master anyways, right? Otherwise what would happen when it tries to push?
So the merge from /merge
ought to be a no-op
Mergify doesn't build the squashed commit.
We could test it. Start the build with git rev-parse HEAD
Mergify doesn't build the squashed commit.
I'm going to go cry in the corner
The file state in the commit that Mergify pushes is exactly the same as the PR branch that Mergify checks. But the git history is different.
And now I don't trust that Travis is actually checking what's in the PR branch.
Travis runs again once a commit is added to master. THAT one should be checked correctly.
Sounds like it's time to look at alternatives
I can potentially look into setting up a Jenkins server. As far as I can see, Jenkins is capable of distributing builds to different servers, so we could share the load if others also have some resources
I guess the problem with moving away from Travis is that this also creates Mergify headaches
So it reached the lint stage a little while ago and started recompiling again. There's no way anything could have changed between the archive and lint stages. The archive took a minute, no commits to master, etc.
I added a line to touch the olean files before the lint stage. Not sure if it will help, but maybe.
If our hypothesis is true and it is getting unpredictable info from the /merge
branch: my impression is this is bizarre, and inefficient, but not fatal.
There's no real connection between Mergify and Travis, any CI with proper GitHub support should work with Mergify.
Yeah... but I don't know how hard it is to get Github support working for self-hosted CI's
The costs of the Travis craziness are slower and occasionally broken PR builds, and maybe it's possible a broken PR could make it to master. The costs of switching to a CI with bad GitHub support are higher, I think.
Git lab has a nice CI infrastructure and it supports github. If Travis is too much of a pain, it can be worth investigating. And the maximum timeout is 3 hours which goes most of the way to building mathlib completely
@Johan Commelin Did you mean running a github server on a local machine? It is a pretty straightforward effort.
A Jenkins server
And it should integrate with the github repo
You can't run github locally can you? I thought it was closed source. Or did they open source it?
I think you can buy a license. Even if it were free, it would definitely not be worth it for us.
There's also "github actions", which should definitely integrate well with github, although it's still in "limited public" beta. https://help.github.com/en/github/automating-your-workflow-with-github-actions/about-github-actions
Each build is allowed to upload some "artifacts", so we might be able to set up olean caches for each PR?
Argh. I'll let it go a bit longer to be sure, but it looks like #1606 is still rebuilding everything. https://travis-ci.org/leanprover-community/mathlib/builds/602507227?utm_source=github_status&utm_medium=notification
I'd expect max 5 min if all the oleans are there already.
How is the linting step relevantly different from the archive step?
You can run a git server. Github is just a collection of servers with a user api.
I ran a private git server on my local net when I was doing security research
I would advise against jumping to that solution. Once we setup our own servers, we have to keep them running, fix the configuration, etc. There are other CI services that we can investigate before we decide to run our own
There is precisely 0% chance we are going to self-host the mathlib git repo.
Github does what lean needs and seems to do it best. I'm not suggesting that you use local servers. I do, but for public work like Axiom, I use github.
For my security work I needed jenkins and git but hosted on a secure subnet. I was just responding to the question of whether it was possible to run git-like services locally.
Nobody wants the extra burden of admin work on a server. I do it, but it is annoying and I don't recommend it unless you have the skills, patience, and nothing else worth doing. :-)
Thanks for clarifying. I'm especially worried about the last one. I think there are plenty of skilled and dedicated people around but there's plenty of other stuff they can look into
AFAICT I don't see any magic options in travis that adjust how it builds PRs. This page mentions the */merge
ref
the only thing I can do is turn different kinds of builds on or off (they are all on), or adjust the .travis.yml
Oh my god, this is so frustrating. I got the linting test to work (i.e., Travis failed due to linting errors) by moving it to the test
stage. Then I changed the linting test to a weaker one that should pass. Now it's running the linting test in the pre-build. It's reusing cached oleans from the previous run, which is fine and expected. But the auto-generated lint_mathlib.lean
shouldn't show up until the test
stage. Is it somehow retrieving the file state from the previous run?
lint_mathlib.lean
isn't part of the git repo. It failed to build in the last run, so there shouldn't be an olean, and even if there were, purge_olean.sh
should delete it.
Is there a way I can see the contents of the directory Travis is working in?
I still have no idea why the separate linting stage was refusing to use the cached oleans.
Hmm. I guess this is the meaning of this line: https://github.com/leanprover-community/mathlib/blob/master/.travis.yml#L17
But shouldn't https://github.com/leanprover-community/mathlib/blob/master/.travis.yml#L38 delete lint_mathlib.lean
?
Which part runs the linting step?
What I would suggest is that you delete lint_mathlib.lean
after you're done using it. This way, it won't make its way into the build cache
I'm solving issues locally. It turns out the file name data/rat/meta.lean
causes issues.
The autogenerated data/rat/all.lean
imports .meta
which parses wrong.
ah! What if you quote it?
I'm going to push a commit renaming that in a sec, which should make the current setup work.
But it still doesn't explain why Travis wanted to build mathlib from scratch when I had the linting step in its own stage.
Did using touch
help?
Nope.
The whole thing is muddled by the fact that Travis actually builds merges with "master." data.rat.meta
didn't even exist on the PR branch so I couldn't figure out locally what was happening.
Is it okay if I merge #1612 directly? I built locally with these changes.
 Maybe that can make things better
Oh, actually, never mind. I don't need to merge that yet, we can let the check run just to be sure.
This has to pass.
Unfortunately, it will fail soon because #1612 missed a data.rat.meta
in test/rat.lean
. I've fixed it in that PR, but not in the lint one yet.
@Rob Lewis Do you want me to rebase travis_lint on rename_rat_meta?
Gah.
I just did, but thanks.
It passed. Proof of concept, we can run a lint test in Travis.
Of course, the script in that PR is a mess now from all my attempts to make it work. And I'm done with this for the weekend.
I just finished an experiment with gitlab. Have a look: https://gitlab.com/simon.hudon/mathlib/commit/5b32a70e3f0006f3f6cc93f836aac533ce89c6ed/pipelines?ref=master
@Rob Lewis I'm trying Azure for lean-depot
. So far, it seems so much faster than Travis or GitLab. I think we might want to consider adopting it for mathlib
Sounds good to me! The free or paid version?
@Simon Hudon GitHub just popped a bunch of balloons in my face about this: https://github.com/features/actions
I usually don't click annoying ads like that out of principle, but it's free for open projects and (presumably) well integrated with GitHub. At a glance, it looks like it could do what we want.
Maybe worth investigating too.
That looks like an exciting tool. Are you thinking of a specific use?
Uh, as far as I can tell can do the same thing as Travis or Azure.
I couldn't find any info about how much time or speed they give you.
Here's a page with some more details on limits: https://help.github.com/en/github/automating-your-workflow-with-github-actions/about-github-actions
Github Actions in fact run on Azure and they are quite similar to Azure Pipelines in most other aspects, but not completely. It is quite confusing.
Are there things that Github Actions can do but Azure can't?
I don't know, I have only looked at Pipelines in detail
{% endraw %}Last updated: Apr 24 2020 at 19:02 UTC


|
G24Lib
A set of convenient classes, functions and other utilities mainly for quickly writing numerical code. Provides relatively easy integration with CUDA, general Runge-Kutta methods, linear equation solvers and more.
|
operator[]
. g24_lib::value_type<C>
equal to Type
). g24_lib::value_type<C>
equal to Type
)? g24_lib::value_type<C>
equal to Type
)? at()
member function in accordance with STL? at()
member function in accordance with STL? g24_lib::value_type<C>
equal to Type
)? g24_lib::value_type<C>
equal to Type
)? g24_lib::value_type<C>
equal to Type
)? g24_lib::value_type<C>
equal to Type
)?


Beta distribution
Alpha and beta sliders can be adjusted using either the mouse or arrow keys (click the slider to select it first if you want to use the arrow keys).
Alpha and beta sliders can be adjusted using either the mouse or arrow keys (click the slider to select it first if you want to use the arrow keys).


Epicodus Track Suggester
Complete for your track path suggestion:
1.) What language are you most interested in?(C#, JavaScript, or Ruby)
2.) Are you most interested in the server-end or front-end?
3.) Which of those choices best fits you (working for a large company on business software, working as an android developer or working for a startup/smaller companies)?
4.)  Which of those three best fits you internal (internal software; high-performance applications or interactive web applications)?
Show My Track
Your trackpath is


--- layout: default --- {% if site.education_in_main %} {% include education.html %} {% endif %} {% include experience.html %} {% include publications.html %} {% include projects.html %} {% include skills.html %}


Cinnabon to Open at Brisbane’s Toombul Shopping Centre in December
Finally, the iconic American bakery has a location for its first Australian outlet.
by Broadsheet EditorsFinally, Cinnabon has revealed the location of its debut Australian store. The US bakery will open at Toombul Shopping Centre in mid-December, it was announced in a media release today.
If you’ve travelled throughout North America you probably know Cinnabon. The iconic chain was established in Seattle in 1985 and as of December 2017 had opened more than 1200 outlets operating across 48 countries. Cinnabon’s killer product? Sticky scrolls fresh-baked every half-hour, covered in Makara cinnamon and drenched in the store’s signature frosting.
Now, it’s coming to Australia, with Cinnabon’s Brisbane launch set to be the first of many in Australia over the next three years. Responsible for the rollout is Bansal Foods, best known for bringing Carl’s Jr to Australia in recent years.
Bansal will bring along the brand’s classic rolls, Caramel Peacanbons, Bonbites, Cinnasweeties and Cinnabon Stix, all washed down with its popular Mochalatta Chill frozen drink.
It’s the latest food and retail coup for Toombul Shopping Centre, which is on a roll with the recent opening of Archie Brothers Cirque Electriq, Little Red Dumpling and Hello Harry.


{% for character in characters %}
{% endfor %}
Connections
{% for connection in character.connections.all %}
{% endfor %}
More
{{connection.contact.first_name}} {{connection.contact.last_name}}
{{connection.opinion}}


The importance and quality of computer science education is becoming a national hot-button issue. In a state where the demand for software developers of applications is consistently a top in-demand job (including in fields like manufacturing), Michigan legislators are recognizing the need to make a change in education to ensure the state has enough worker supply to meet the growing demand. According to code.org, nine out of 10 parents want their children to learn computer science, but only one in four schools teach computer science.
Michigan is working to pass legislation that will allow students to replace foreign language classes by learning computer programming, or coding languages, instead. Michigan has taken a few other important steps toward increasing the number of students that are interested and skilled in computer sciences, including allowing computer science to count toward core education requirements (one of 29 states to do so), as well as allowing it to count as an admission requirement for postsecondary education institutions. This newer piece of legislation is seen by supporters as a way to increase the number of computer science courses offered and taken advantage of by students in hopes they will follow this profitable and necessary career path.
While this legislation is a step in the right direction for Michigan, there are some misconceptions surrounding the purpose of the substitution. Some believe the ability to substitute credit for coding over foreign language means the supporting educators and legislators believe learning to code produces the same educational results as learning a foreign language. This is not the case. For example, in a foreign language course, students learn not just the language but also the culture and history of the geographic areas they are studying, while learning to program and code emphasizes logic skills and shares more similarities with math and science courses.
Supporters generally do not believe that learning to code is the same thing as learning a foreign language. The reason for supporting the proposed legislation is that it would allow students to choose their electives more effectively, and students interested in taking a foreign language and computer science courses could still do so.
Many other strategies exist to continue supporting computer science learning for Michigan students. The state does not yet require that all high schools offer computer science, does not require computer science for graduation, and does not provide dedicated funding for professional development for educators in computer science. While these options may be on the horizon, they each come with challenges. For example, requiring all secondary schools to offer computer science raises the question as to whether all secondary schools have the funds to support the technology required to teach computer science or qualified teachers to teach the subject.
There is much work to do around improving access to and quality in computer science education, but Michigan is on the forefront of making legislative changes to support these efforts. Though all may not agree that computer science should replace foreign language credits, giving Michigan students the choice may give them career options they may not otherwise have had.
Article by Crain's Detroit posted July 26th, 2016: http://www.crainsdetroit.com/article/20160726/BLOG107/160729899/proposed-curriculum-change-is-code-for-success


HexEdit displays a list of currently open windows at the bottom of the Window menu. A check mark appears in front of the name of the active window. Choose a window from this list to make its window active. You can also flip through all the open windows with the Next Window command (Ctrl+F6).
Shortcuts
Mouse: Click on a visible part of the desired window to activate it, or click on the tab for the window at the top or bottom of the HexEdit display if enabled (see Window Display Options page).


This section gives the community a space to provide information on setting up, managing, and maintaining JupyterHub.
Important
We recognize that Kubernetes has many deployment options. As a project team with limited resources to provide end user support, we rely on community members to share their collective Kubernetes knowledge and JupyterHub experiences.
Note
Contributing to Z2JH. If you would like to help improve the Zero to JupyterHub guide, please see the issues page as well as the contributor guide.
We hope that you will use this section to share deployments with on a variety of infrastructure and for different use cases. There is also a community maintained list of users of this Guide and the JupyterHub Helm Chart.
Please submit a pull request to add to this section. Thanks.
Community section


I've also completed some projects such as posters and sketches. I spend most of my time doing digital art, but it's nice to occasionally go back to pen & paper once in a while!


Serial Mom
Written and Directed by John Waters
Starring Kathleen Turner, Sam Waterson, Ricki Lake, Matthew Lillard, Scott Wesley Morgan, Walt MacPherson, Justin Whalin, and Patricia Dumnock
As Reviewed by James Brundage (MovieKritic2000)
In famous words: they don't make em like they used to.
When they used to make serial killer movies, the serial killers were guys. When they used to make serial killer movies, the serial killers used an axe or a chainsaw. When they used to make serial killer movies, the serial killers weren't happily married with children.
Hey, things change, and change is good.
Serial Mom is a serial killer so different from the norm that you have to laugh out loud. Sure, its got enough gore to satisfy any horror fan, but it also has a nice satiric edge to it, one that will make anyone with a dark sense of humor laugh.
Taking a stab (sorry, couldn't resist) at the golden age of television, you have Beverly Sutphin (Kathleen Turner), who appears to be a nice mother on the surface but inside is a completely deranged serial killer. The motives for her crimes are silly breakings of social convention (cutting people off in the parking lot of Jo-Anne's fabric, standing a girl up at a flea market, eating chicken, wearing white shoes after labor day, etc.), to which she responds with a viscous psychopathic murder spree (is there any other kind?).
Her son is obsessed with horror movies, her husband a mild mannered dentist. Her daughter is a social reject, and she is a pillar of the community.
The film goes incredibly fast, displaying the time periodically at the bottom of the screen, so as you are constantly aware of how quickly the story is progressing in the scary world that the movie creates. As she kills, evades police officers, and goes on car chases, Beverly acts as if it was all a game (she's smiling and giggling all the time).
Almost a precursor to Scream (which ironically also featured Matthew Lillard), Serial Mom also picks on horror movies. A trio of teenagers is always watching them, and the movies are what initially piqued Beverly's fascination with gore. Of course, she only likes gore in the movies. When the time comes that she has to remove a bodily organ from the end of a fire poker, she's all "ewww."
A warning for potential viewers of this film: you must have a dark sense of humor. I'm not talking pseudo-dark. I'm not talking "I thought Scream was funny" dark. I'm talking laughed like Robert DeNiro in Cape Fear during Very Bad Things dark. You've got to be able to find humor in the most pessimistic of situations, while keeping your mind open to the general gist of the movie (the McCarthy era was that of complete repression, which has potentially insane side effects), and that's very tough.
Another warning, this film is not for the weak of stomach. It's got gore all through, and has enough violence to generate a lobbyist feeding frenzy.
This film should also probably be seen as a warning against those that are fascinated and deify the violence on the screen.  It can function as a raw horror movie, but can only be truly appreciated outside of the realm of campy teenage viewing. Half of the jokes are too old for most teenagers to get, anyway.
Kathleen Turner shines as the psychopath, giving one of the most memorable performances as a villain in the 90s. Sam Waterson crawls out of his usual "Law & Order" shell as the husband of a serial killer. Mathew Lillard reminds me of Nicole Kidman's character in To Die For: someone willing to ride the hype wave of a murder for all that its worth. Ricki Lake actually gives a half decent performance, but she's under the skillful direction of John Waters (Pecker).
If you're not weak of stomach, heart, or mind, go see Serial Mom. If you are weak in any one of these three aspects, the film will murder you.
The review above was posted to the
rec.arts.movies.reviews newsgroup (de.rec.film.kritiken for German reviews).
The Internet Movie Database accepts no responsibility for the contents of the
review and has no editorial control. Unless stated otherwise, the copyright
belongs to the author.
Please direct comments/criticisms of the review to relevant newsgroups.
Broken URLs inthe reviews are the responsibility of the author.
The formatting of the review is likely to differ from the original due
to ASCII to HTML conversion.
Related links: index of all rec.arts.movies.reviews reviews


If you don't get 78% or more on your final, you won't pass.
Save a bundle at our big yearend sale.
When the dialog box is displayed, enter brock21.
The chemical symbol for water is H2O.
To sleep, perchance to dream-ay, there's the rub.


Pat's Seattle Salmon Cookies
All Salmon, None of the Taste
MENU
ORDER NOW
COMING SOON
OFFERS
COMING SOON
MEMBERS
COMING SOON
Address
Minimum Customers per Hour
Maximum Customers per Hours
Average Cookies Sold per Customer
Times
Daily Location Totals
Locations
Totals


In orderd to start an animation you need to add to your element:
START | ANIMATION TYPE | DURATION | DELAY (optional) | CUBIC BEZIER (optional)
Example:

Skelet.

style="--duration: 1s"
Define animation duration
style="--delay: 1s"
Define animation delay [optional]
style="--ease: ..."
Define your own rate of change over time.
i.e. Cubic Bezier [optional]
start
/.animate
To start an animation you need either one or the other.
.invisible
/.hide
Setting element's opacity to 0, good for hiding elements when animation starts.
.infinite
/.loop
Loops the animation forever
.reverse
Specifies whether an animation should play in reverse direction
.alternate
The animation will be played as normal every odd time (1,3,5,etc..) and in reverse direction every even time (2,4,6...)
.alternate-reverse
The animation will be played in reverse direction every odd time (1,3,5,etc..) and in a normal direction every even time (2,4,6,etc...)
Objects in real life don’t just start and stop instantly, and almost never move at a constant speed. This is why now we offer you Cubic Bezier to spiece up your aminations and bring them to that new new next next level
Cubic Bezier is set by adding ease=easeInSine
to your element.
Cubic Bezier can be also used inside your transition:;
h1{transition: all 1s var(--easeInOutQuad);}
ease=easeInSine
ease=easeOutSine
ease=easeInOutSine
ease=easeInQuad
ease=easeOutQuad
ease=easeInOutQuad
ease=easeInCubic
ease=easeOutCubic
ease=easeInOutCubic
ease=easeInQuart
ease=easeOutQuart
ease=easeInOutQuart
ease=easeInQuint
ease=easeOutQuint
ease=easeInOutQuint
ease=easeInExpo
ease=easeOutExpo
ease=easeInOutExpo
ease=easeInCirc
ease=easeOutCirc
ease=easeInOutCirc
ease=easeInBack
ease=easeOutBack
ease=easeInOutBack
Example:

animation=fadein
animation=fadein-up
animation=fadein-down
animation=fadein-right
animation=fadein-left
animation=fadeout
animation=fadeout-down
animation=flash
animation=pulse
animation=shake
animation=wobble
animation=rollin
animation=rollout
animation=zoomin
animation=zoomout
animation=zoomin-down
animation=bounce
animation=bouncein
animation=scalein
animation=flip
animation=flipin-x
animation=flipout-x
animation=flipin-y
animation=flipout-y


| Home | Trees | Indices | Help |
|---|
|
|
object --+ | GenericBibJSON
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
|||
|
Inherited from |
|
|||
| title | |||
| keywords | |||
|
Inherited from |
|
x.__init__(...) initializes x; see help(type(x)) for signature
|
|
title
|
keywords
|
| Home | Trees | Indices | Help |
|---|
| Generated by Epydoc 3.0.1 on Fri Feb 28 17:57:31 2014 | http://epydoc.sourceforge.net |


Last amended: 16 May 2023, app version 1.43
This privacy notice explains how your data is processed and what data protection rights you have when you use the CovPassCheck app to verify digital COVID Certificates.
Digital COVID Certificates have been valid within the entire European Union (EU) since 1 July 2021 as certification of COVID-19 vaccination and testing, and of recovery from a confirmed case of COVID-19. The official name is “EU Digital COVID Certificate” (certificate).
This privacy notice covers the following topics:
This app is published by the Robert Koch Institute (RKI) for the German Federal Government. The RKI is also responsible for ensuring that your personal data is processed in compliance with data protection regulations.
Using the app is voluntary. There are other acceptable ways to check vaccination, test, or recovery certificates.
The app allows you to verify whether other people’s certificates are valid and prove a complete vaccination protection.
To do this, you can use the CovPassCheck app to scan the QR code displayed on a certificate presented to you, in order to ascertain whether that certificate is valid. The QR code contains an electronic signature of the national issuer (in Germany, the issuer is the RKI). The electronic signature is generated by the RKI when creating the certificate, on the basis of the data about the certificate holder which is contained in the certificate. The signature is a special type of encryption that allows the RKI to confirm that the certificate is an official digital document created by the RKI.
The RKI also provides the corresponding public keys and revocation lists. The public keys and revocation lists can be used to check whether a certificate’s electronic signature actually originates from the RKI and whether the certificate has been revoked or manipulated since being signed electronically.
The CovPassCheck app regularly downloads the RKI’s public keys and revocation lists in the background and stores them locally on your smartphone. This allows the app to regularly check the validity of the electronic signature and thus the authenticity of certificates that are checked. The public keys do not contain any personal data. The revocation lists only contain a revocation identifier for a revoked certificate in the form of special one-way encryption (what’s known as a hash value). The revocation identifier cannot be used to infer the certificate data or other information about a particular person.
In order to be able to detect date manipulations in certificates, the date and time set in the smartphone is compared with the real-time information of a freely available time server.
Please note that you are only authorised to have someone else present their certificate for verification to the extent permitted by law.
If you scan a certificate and read data in the process, you are responsible for compliance with data protection regulations.
In order to download the public keys for authenticating the electronic signature and revocation lists, a connection regularly needs to be established to an RKI server. The server has to process technical access data for this purpose. This data includes the following:
This access data is processed to enable and secure the connection and data exchange between the app and the server. You will not be identified personally as a user of the CovPassCheck app and no user profile will be created. Your IP address will not be stored beyond the end of the individual usage procedure.
Access data is also processed to compare the date and time with the time server.
The RKI will only process your data if it has a legal basis for doing so. The processing of your access data as described in this privacy notice is necessary to technically implement the verification of the validity of the certificates. The legal basis for the processing of your access data is Sect. 3 of the German Federal Data Protection Act (BDSG) and Art. 6(1) Sentence 1(e) of the General Data Protection Regulation (GDPR).
The CovPassCheck app requires access to your smartphone camera when you scan the QR code to verify a certificate. The app also requires an internet connection in order to download the latest key information and updates according to section 4 from the RKI server system. For information about other permissions the app may request, please refer to the FAQ section in the app.
The app will not permanently store the QR codes scanned by you, or the information read from them, on your smartphone. Nor will the RKI permanently store any personal data on the app’s server system.
The RKI has commissioned the company KDO Service GmbH (KDO) to operate and maintain the server system. KDO processes the personal data on behalf and at the instruction of the RKI (meaning it is what’s known as a processor under data protection law). Contractual safeguards are in place to ensure that the data protection requirements are met.
To ensure the correct time setting, the current time is obtained from a freely available, randomly selected time server from the NTP Pool project (region de.pool.ntp.org). Here access data is temporarily processed.
If the RKI processes your personal data, you have the following data protection rights:
Please note that the RKI can only fulfil the rights mentioned above if data to which the asserted claims relate is processed on an ongoing basis. This would only be possible if personal data were stored after being transmitted to the RKI server. This is not necessary for the purposes of the app. For this reason, the aforementioned data protection rights under Art. 15, 16, 17, 18 and 21 GDPR are largely redundant.
If you have any questions or concerns regarding data protection in connection with the CovPassCheck app, you are welcome to send them to the RKI’s official data protection officer by post to: Robert Koch-Institut, FAO the data protection officer, Nordufer 20, 13353 Berlin, or by emailing datenschutz@rki.de.


BuzzFeed UK threatened with being dissolved over late accounts
BuzzFeed UK has been told it will be dissolved in two months if it fails to file its accounts with Companies House.
The warning comes after the online media organisation missed a deadline at the end of September to submit its financial information for 2018.
On Monday, a “First Gazette” notice was issued for a compulsory strike-off.
The notice says: “The Registrar of Companies gives notice that, unless cause is shown to the contrary, the company will be struck off the register and dissolved not less than two months from (December 10).”
Julie Palmer, insolvency expert at Begbies Traynor, said: “Receiving a notice like this is more common than you might think, but it’s not often a cause for concern without any clear reasons behind it.”
These could include extending the company’s accounting period, although Companies House must still be informed, and most experts agree an accounting extension is typically a sign of financial difficulties.
The period covered in the late BuzzFeed UK accounts covers a difficult year for the business, with revenues failing to match expectations.
In January this year, founder and chief executive Jonah Peretti announced that 15% of the workforce worldwide would be laid off to cut costs.
It came weeks after UK editor-in-chief Janine Gibson stepped down after three-and-a-half years in charge and followed calls from staff to unionise.
BuzzFeed, which was launched in the US in 2006, attempted a major overseas expansion in recent years. But it subsequently retrenched, along with cutting back its US operations.
Despite heavy cuts to its UK workforce, it has managed to bag some major scoops and awards, including being named news website of the year in 2018.
BuzzFeed UK also uncovered a series of troubling deaths of Russians in the UK, leading to the reopening of police investigations, and reporters also exposed a series of issues at the Department of Justice.
A spokeswoman for BuzzFeed UK said accounts would be filed “soon” but declined to specify.
In 2017 the business made a pre-tax loss of £1.9 million on turnover of £33.4 million, although the accounts said it continues to be financially supported by its US parent company.
In 2016 it made a pre-tax loss of £3.3 million on revenues of £20.5 million.


Hello, and welcome to my blog! I'm KaadmY. I make stuff and play games. This website is generated with Jekyll and hosted on Github. Back to blog index


seagrass change European area sites density seagrasses coastal losses water recovery [], trajectory metrics {border-style species px;} #ffffff;} Sea data loss meadows (Fig. decline extent marina quality depth Fig. Zostera causes rate time Supplementary compiled included increase noltei oceanica Data changes decadal declining gains grid.. site trajectories Seagrass available global management ha Europe Mediterranean University rates reported reversal specific (%), Directive Posidonia Science area, conservation improvement increasing number Department final http://orcid.org/--- largest net nutrient px; showing using {font-family Atlantic Europe, LINK Mar. Technology Wadden attributed based ecosystem ecosystems font-size series status wasting (%) (). (including Aquat. Duarte Statistical actions analysis compilation decades decline, different double; including information limits natural nodosa, recent sources trend (Supplementary (e.g., ./s--- Decadal Foundation Funding Marbà Marine Nature Number R.S. Research Sci. Source Water areas assess assessment assessments border-color border-width climate coasts combination decade defined density, disease ecological end given increase, indicators mainly marine nodosa oceanica, overall percentage protection reduction reporting sewage, shoot showed sites, solid; total trends waters {font-style {font-weight ./j.marpolbul... Baltic Bot. Bull. C.B.d.l.S. Change Commons Council Creative Cymodocea Environmental Estuar. Institute Ministry N.M., Official Portuguese Santos Sciences, Spanish T.A., Unsworth WFD bold century change, classified consecutive continental courier; declines declining, degradation documented em; evolution important improving increasing, large lost lower marina, maximum mechanical metric monitoring pt;} quality, reports respectively. revealed review slowdown source, studies support supported values whiskers −),


Girls just wanna go fun and enjoy.
Paorama , SanFransisco
Sold imported car with best price
Yes, we do best deals
strong bids gives good prices
We built strong auctions
Yes, best collection is ours
Sold upto 30,000 vehicles


Select image you want a story from
Type sentences you want to influence image (don't forget the "." to end them)
Type sentences you want to write a story from (don't forget the "." to end them)
Generated passage :


Free groups, Lengths and Computer Proofs
Siddhartha Gadgil
Indian Institute of Science
joint with
the rest of (spontaneous) polymath 14
The PolyMath 14 participants
- Tobias Fritz, MPI MIS
- Siddhartha Gadgil, IISc, Bangalore
- Apoorva Khare, IISc, Bangalore
- Pace Nielsen, BYU
- Lior Silberman, UBC
- Terence Tao, UCLA
- On Saturday, December 16, 2017, Terrence Tao posted on his blog a question, which Apoorva Khare
had asked him.
Is there a homogeneous, (conjugacy invariant) length function on the free group on two
generators?
- Six days later, this was answered in a collaboration involving several
mathematicians (and a computer).
- This the story of the answer and its discovery.
Length functions
- Fix a group $G$, i.e. a set with an associative product with inverses.
- A pseudo-length function $l: G \to [0, \infty)$ is a function such
that:
- $l(e) = 0$.
- $l(g^{-1}) = l(g)$ , for all $g \in G$.
- (Triangle inequality) $l(gh) \leq l(g) + l(h)$, for all $g,h\in G$.
- A length function is a pseudo-length function such that $l(g) > 0$
whenever $g\neq e$ (positivity condition).
Conjugacy-invariance and Homogeneity
- A pseudo-length function $l$ is said to be conjugacy invariant if
$l(ghg^{-1})=l(h)$ for all $g,
h \in G$.
- Conjugacy often corresponds to change of coordinates.
- $l$ is said to be homogeneous if $l(g^n) = nl(g)$ for all $g \in G$.
- Homogeneity was motivated by norms on vector spaces.
Length functions on $\mathbb{Z}^2$
- The group $(\mathbb{Z}^2, +) = \{(n, m) : n, m \in \mathbb{Z}\}$ with
$(n_1, m_1) + (n_2, m_2) = (n_1 + n_2, m_1 + m_2)$.
-
Two length functions on $\mathbb{Z}^2$ are:
- $l_1((a,b)) = |a| + |b|$,
- $l_2((a, b)) = \sqrt{a^2 + b^2}$
- These are homogeneous (and conjugacy invariant).
- The function $l'((a, b)) = \sqrt{|a|} + \sqrt{|b|}$ is a length function, but
not homogeneous.
- The function $l''((a, b)) = |a - b|$ is a homogeneous pseudo-length function
which is not positive.
Groups without homogeneous length functions
- If $l$ is a homogeneous length function on $G$ and $g\in G$ is such that
$g^n=e$ then $l(g)=0$ as $nl(g) =
l(g^n) = 0$.
- Thus, if $G$ has torsion, i.e., there exists $g\neq e\in G$, such that
$g^n =e$ for some $n > 0$ and $g\neq e$, then there is no homogeneous length function on $G$.
- In particular finite groups have no homogeneous length functions.
Free group $\mathbb{F}_2$ on $\alpha$, $\beta$
- Consider words in four letters $\alpha$, $\beta$, $\bar{\alpha}$ and
$\bar{\beta}$.
- We multiply words by concatenation, e.g. $\alpha\beta\cdot\bar{\alpha}\beta =
\alpha\beta\bar{\alpha}\beta$.
- Two words are regarded as equal if they can be related by cancelling adjacent
letters that are inverses, e.g. $\alpha\beta\bar{\beta}\alpha\beta = \alpha\alpha\beta$.
- This gives a group;
- the identity is the empty word
- every word has an inverse, e.g.,
$(\alpha\bar{\beta}\alpha\beta\beta)^{-1} =
\bar{\beta}\bar{\beta}\bar{\alpha}\beta\bar{\alpha}$.
Word length on $\mathbb{F}_2$
- Any word is equivalent to a unique reduced word, i.e., where we have no cancellation e.g. $\alpha\beta\bar{\beta}\alpha\beta\bar{\beta}\beta\bar{\alpha}$ reduces to $\alpha\alpha\beta\bar{\alpha}$.
- The word length $l_0$ on $\mathbb{F_2}$ is the length of the reduced
word
representing an element.
- The word length is not conjugacy-invariant as $l_0(\alpha\beta\bar{\alpha}) = 3
\neq 1 = l_0(\beta)$.
- The word length is also not homogeneous, e.g.,
$l_0((\alpha\beta\bar{\alpha})^2) = l_0(\alpha\beta\beta\bar{\alpha}) = 4 \neq
2l_0(\alpha\beta\bar{\alpha})$.
Pullback pseudo-length on $\mathbb{F}_2$
- We define a homomorphism $ab: \mathbb{F}_2 \to \mathbb{Z}^2$.
- For a word $g$, let $n_\alpha(g)$ and $n_\beta(g)$ be the number of $\alpha$'s and
$\beta$'s counted with sign.
- Define $ab(g) = (n_\alpha(g), n_\beta(g))$, e.g.
$ab(\alpha\alpha\beta\bar{\alpha}\bar{\beta}\alpha\bar{\beta}) = (2, -1)$.
- We get a pullback pseudo-length $l$ on $\mathbb{F}_2$ by $l_{ab}(g) =
l_1(ab(g)) = |n_\alpha(g)| + |n_\beta(g)| $.
- As $l_1$ is homogeneous, so is $l_{ab}$.
- However, this is not a length function as $l_{ab}([\alpha,
\beta]) = l(\alpha\beta\bar{\alpha}\bar{\beta}) =0$, violating positivity (recall $[g, h] = ghg^{-1}h^{-1}$).
The Main results
- Question: Is there a homogeneous length function on the free
group on two generators?
- Answer: No; we in fact describe all
homogeneous pseudo-lengths.
-
Theorem: Any homogeneous pseudo-length function on a group $G$ is the pullback
of a pseudo-length on its abelianization $G / [G, G]$.
- Corollary: If $G$ is not abelian (e.g. $G = \mathbb{F}_2$)
there is no homogeneous length function on $G$.
- In fact, every homogeneous pseudo-length is the pullback of a norm on
a vector space.
Lengths from Non-crossing matchings
- Given a word in $\mathbb{F}_2$, we consider matchings such that
- letters are paired with their inverses,
- there are no crossings
- The energy is the number of unmatched letters.
Watson-Crick length on $\mathbb{F}_2$
- For $g\in \mathbb{F}_2$, define the Watson-Crick
length $l^{}_{WC}(g)$
to be the minimum number of unmatched letters over all non-crossing matchings.
- $l^{}_{WC}$ is
unchanged under cancellation (hence well-defined
on $\mathbb{F}_2$) and
conjugacy invariant.
- In fact it is the maximal
normalized conjugacy-invariant length
function on $\mathbb{F}$. Candidate?
- However, if $g=\alpha[\alpha, \beta]$, then
$l^{}_{WC}(g^2)= 4$, but
$l^{}_{WC}(g) = 3$, violating homogeneity.
The great bound chase
- By Tuesday morning, most people were convinced that there are no homogeneous
length functions on the free group, and probably $l([\alpha, \beta]) = 0$ for homogeneous pseudo-lengths.
- There was a steady improvements in the combinatorial/analytic bounds on
$l([\alpha, \beta])$.
- These seemed to be stuck above 1 (as observed by Khare) - but eventually broke
this barrier (work of Fritz, Khare, Nielsen, Silberman, Tao).
- At this stage, my approach diverged.
Computer Assisted proofs: beyond (symbolic) computation, enumeration?
- We can recursively compute the Watson-Crick length $l^{}_{WC}(g)$ for a word
$g$.
- This gives an upper bound on all conjugacy-invariant normalized lengths.
- This can be combined with using homogenity.
- Using this, I obtained an upper bound of about $0.85$ on $l(\alpha, \beta)$.
- This was upgraded to a (computer) checkable proof.
- On Thursday morning, I posted an in principle
human readable proof of a bound.
- The computer-generated proof was studied by Pace Nielsen, who extracted the internal
repetition trick.
- This was extended by Nielsen and Fritz and generalized by Tao; from this Fritz
obtained the key lemma:
- Let $f(m, k) = l(x^m[x, y]^k)$. Then $f(m, k) \leq\frac{f(m-1, k) + f(m+1,
k-1)}{2}$.
- A probabilistic argument of Tao finished the proof. [Algebra Number Theory , 12 (2018), 1773-1786.]
- Lemma: If $x = s(wy)s^{-1} = t(zw^{-1})t^{-1}$, we have $l(x)\leq \frac{l(y)+
l(z)}{2}$.
- Proof: $l(x^nx^n) = l(s(wy)^ns^{-1}t(zw^{-1})^nt^{-1})$ $\leq
n(l(y) +l(z)) + 2(l(s) + l(t))$
- Use $l(x) = \frac{l(x^nx^n)}{2n}$ and take limits.
- Lemma: $f(m, k) \leq\frac{f(m-1, k) + f(m+1, k-1)}{2}$, where $f(m, k) =
l(x^m[x, y]^k)$.
- In other words, for $Y$ a Rademacher random variable, i.e., $Y$ is $1$ or $-1$
each with probability $1/2$,
$f(m, k)\leq E(f( (m, k - 1/2) + Y(1, -1/2) ))$.
- Hence for $Y_i$ i.i.d. Rademacher random variables, $f(0, n) \leq E(f((Y_1 +
Y_2 + \dots + Y_{2n}) (1, -1/2) ))$,
- By triangle inequality, $f(a, b) \leq A\Vert (a, b) \Vert$.
- $Y_1 + Y_2 + \dots Y_{2n}$ has mean $(0, 0)$ and variance $2n$, so $E(\Vert Y_1
+ Y_2 + \dots Y_{2n} \Vert) \leq B\sqrt{n}$.
- We deduce that $l([x, y]^n) = f(0, n) \leq C\sqrt{n}$, hence $l([x, y]) = 0$.
Computer bounds and proofs
- For $g=ah$, $a \in \{\alpha, \beta, \bar{\alpha}, \bar{\beta}\}$, the length
$l^{}_{WC}(g)$ is the minimum of:
- $1 + l^{}_{WC}(h)$ : corresponding to $a$
unmatched.
- $\min\{l^{}_{WC}(x) + l^{}_{WC}(y): h =
x\bar{a}y \}$.
- We can describe a minimal non-crossing matching by a similar recursive
definition.
- A similar recursion gives a proof of a bound on $l(g)$ for $g$ a
homogeneous, conjugacy-invariant length with $l(\alpha)=l(\beta)=1$.
- We can also use homogeneity for selected elements and powers to bound the
length function $l$.
Conclusions
- If we view applications of the axioms as moves, the computer proof helped in
identifying composite moves that could be applied recursively.
-
The principal difficulty in finding computer proofs often lies in choosing the useful complexity
increasing moves (here homogeneity).
- In this case, these were chosen mainly on mathematical considerations.
- However, a general heuristic we see is to seek useful families of
complexity-increasing moves.
Conclusions
-
The unusual feature of the use of computers here was that a computer generated but human
readable proof was read, understood, generalized
and abstracted by mathematicians to obtain the key lemma in an interesting
mathematical result.
-
The use of computers was based on the idea of proofs as mathematical objects which can be
computed, following foundations based on Homotopy Type Theory.


Email: {{email}}
Address: {{address.fullAddress}}
Hobbies: {{hobbies}}
Hobbies in list: {{showHobbies ? 'Hide Hobbies' : 'Show Hobbies'}} Add to Hobbies